diff --git a/CHANGELOG b/CHANGELOG
index 4148240e2..c87ad9522 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -2,6 +2,7 @@
 
 * SystemVerilog: typedefs from package scopes
 * SystemVerilog: assignment patterns with keys for structs
+* SMV: LTL V operator
 
 # EBMC 5.5
 
diff --git a/regression/smv/LTL/smv_ltlspec_R1.desc b/regression/smv/LTL/smv_ltlspec_R1.desc
index 3233a406a..76afd2702 100644
--- a/regression/smv/LTL/smv_ltlspec_R1.desc
+++ b/regression/smv/LTL/smv_ltlspec_R1.desc
@@ -1,12 +1,12 @@
 CORE
 smv_ltlspec_R1.smv
 --bound 10
-^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$
-^\[.*\] FALSE R x != 4: PROVED up to bound 10$
-^\[.*\] x = 2 R x = 1: REFUTED$
-^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: PROVED up to bound 10$
-^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: REFUTED$
-^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: PROVED up to bound 10$
+^\[.*\] x >= 1 V x = 1: PROVED up to bound 10$
+^\[.*\] FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1: REFUTED$
+^\[.*\] x >= 1 V x = 1 & FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1 & x >= 1 V x = 1: REFUTED$
+^\[.*\] x = 2 V x = 1 \| x >= 1 V x = 1: PROVED up to bound 10$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/LTL/smv_ltlspec_R2.desc b/regression/smv/LTL/smv_ltlspec_R2.desc
index d8b4df170..315328cc0 100644
--- a/regression/smv/LTL/smv_ltlspec_R2.desc
+++ b/regression/smv/LTL/smv_ltlspec_R2.desc
@@ -1,7 +1,7 @@
 KNOWNBUG broken-smt-backend
 smv_ltlspec_R2.smv
 --bound 10
-^\[.*\] FALSE R x != 3: REFUTED$
+^\[.*\] FALSE V x != 3: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
 ^x@1 = 2$
diff --git a/regression/smv/LTL/smv_ltlspec_R3.desc b/regression/smv/LTL/smv_ltlspec_R3.desc
index 55688211b..aadef15ee 100644
--- a/regression/smv/LTL/smv_ltlspec_R3.desc
+++ b/regression/smv/LTL/smv_ltlspec_R3.desc
@@ -1,7 +1,7 @@
 CORE
 smv_ltlspec_R3.smv
 --bound 1
-^\[.*\] FALSE R x != 3: PROVED up to bound 1$
+^\[.*\] FALSE V x != 3: PROVED up to bound 1$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/LTL/smv_ltlspec_R4.desc b/regression/smv/LTL/smv_ltlspec_R4.desc
index 7671d6989..6d0ede9d0 100644
--- a/regression/smv/LTL/smv_ltlspec_R4.desc
+++ b/regression/smv/LTL/smv_ltlspec_R4.desc
@@ -1,7 +1,7 @@
 CORE
 smv_ltlspec_R4.smv
 --bound 10
-^\[.*\] FALSE R x != 0: PROVED up to bound 10$
+^\[.*\] FALSE V x != 0: PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/smv/LTL/smv_ltlspec_V1.desc b/regression/smv/LTL/smv_ltlspec_V1.desc
new file mode 100644
index 000000000..c72a0229a
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V1.desc
@@ -0,0 +1,14 @@
+CORE
+smv_ltlspec_V1.smv
+--bound 10
+^\[.*\] x >= 1 V x = 1: PROVED up to bound 10$
+^\[.*\] FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1: REFUTED$
+^\[.*\] x >= 1 V x = 1 & FALSE V x != 4: PROVED up to bound 10$
+^\[.*\] x = 2 V x = 1 & x >= 1 V x = 1: REFUTED$
+^\[.*\] x = 2 V x = 1 \| x >= 1 V x = 1: PROVED up to bound 10$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/smv/LTL/smv_ltlspec_V1.smv b/regression/smv/LTL/smv_ltlspec_V1.smv
new file mode 100644
index 000000000..851abde59
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V1.smv
@@ -0,0 +1,19 @@
+MODULE main
+
+VAR x : 0..10;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x>=3 : 3;
+      TRUE: x+1;
+    esac;
+
+LTLSPEC x >= 1 V x = 1 -- should pass
+LTLSPEC FALSE V x != 4 -- should pass
+LTLSPEC x = 2 V x = 1 -- should fail
+LTLSPEC (x >= 1 V x = 1) & (FALSE V x != 4) -- should pass
+LTLSPEC (x = 2 V x = 1) & (x >= 1 V x = 1) -- should fail
+LTLSPEC (x = 2 V x = 1) | (x >= 1 V x = 1) -- should pass
diff --git a/regression/smv/LTL/smv_ltlspec_V2.desc b/regression/smv/LTL/smv_ltlspec_V2.desc
new file mode 100644
index 000000000..66afee767
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V2.desc
@@ -0,0 +1,14 @@
+KNOWNBUG broken-smt-backend
+smv_ltlspec_V2.smv
+--bound 10
+^\[.*\] FALSE V x != 3: REFUTED$
+^Counterexample with 3 states:$
+^x@0 = 1$
+^x@1 = 2$
+^x@2 = 3$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The trace has too many states.
diff --git a/regression/smv/LTL/smv_ltlspec_V2.smv b/regression/smv/LTL/smv_ltlspec_V2.smv
new file mode 100644
index 000000000..dc6781b8d
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V2.smv
@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3
+LTLSPEC FALSE V x != 3
diff --git a/regression/smv/LTL/smv_ltlspec_V3.desc b/regression/smv/LTL/smv_ltlspec_V3.desc
new file mode 100644
index 000000000..08d514d34
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V3.desc
@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_V3.smv
+--bound 1
+^\[.*\] FALSE V x != 3: PROVED up to bound 1$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/smv/LTL/smv_ltlspec_V3.smv b/regression/smv/LTL/smv_ltlspec_V3.smv
new file mode 100644
index 000000000..1b9e20bb8
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V3.smv
@@ -0,0 +1,16 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- trace should be 1, 2, 3
+-- hence no trace with k=1
+LTLSPEC FALSE V x != 3
diff --git a/regression/smv/LTL/smv_ltlspec_V4.desc b/regression/smv/LTL/smv_ltlspec_V4.desc
new file mode 100644
index 000000000..285263d39
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V4.desc
@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_V4.smv
+--bound 10
+^\[.*\] FALSE V x != 0: PROVED up to bound 10$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/smv/LTL/smv_ltlspec_V4.smv b/regression/smv/LTL/smv_ltlspec_V4.smv
new file mode 100644
index 000000000..e6b0e7a65
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_V4.smv
@@ -0,0 +1,15 @@
+MODULE main
+
+VAR x : 0..3;
+
+ASSIGN
+  init(x) := 1;
+
+  next(x) :=
+    case
+      x=3 : 3;
+      TRUE: x+1;
+    esac;
+
+-- should pass
+LTLSPEC FALSE V x != 0
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index 76ff633ec..ce2c9b5c9 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -566,7 +566,7 @@ bool expr2smvt::convert(
 
   else if(
     src.id() == ID_AU || src.id() == ID_EU || src.id() == ID_AR ||
-    src.id() == ID_ER || src.id() == ID_U || src.id() == ID_R)
+    src.id() == ID_ER || src.id() == ID_U)
   {
     return convert_binary(
       to_binary_expr(src),
@@ -575,6 +575,13 @@ bool expr2smvt::convert(
       precedence = precedencet::TEMPORAL);
   }
 
+  else if(src.id() == ID_R)
+  {
+    // LTL release is "V" in NuSMV
+    return convert_binary(
+      to_binary_expr(src), dest, "V", 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 1a285fe61..a90bbd31e 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 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 X_Token
 %left  EQUAL_Token NOTEQUAL_Token LT_Token GT_Token LE_Token GE_Token
 %left  union_Token
 %left  IN_Token NOTIN_Token
@@ -621,6 +621,7 @@ term       : variable_name
            | X_Token  term            { init($$, ID_X);  mto($$, $2); }
            | term U_Token term        { binary($$, $1, ID_U, $3); }
            | term R_Token term        { binary($$, $1, ID_R, $3); }
+           | term V_Token term        { binary($$, $1, ID_R, $3); }
            | term EQUAL_Token    term { binary($$, $1, ID_equal, $3); }
            | term NOTEQUAL_Token term { binary($$, $1, ID_notequal, $3); }
            | term LT_Token       term { binary($$, $1, ID_lt, $3); }