diff --git a/regression/ebmc/neural-liveness/counter1.desc b/regression/ebmc/neural-liveness/counter1.desc
index 772342a5f..67697ed1e 100644
--- a/regression/ebmc/neural-liveness/counter1.desc
+++ b/regression/ebmc/neural-liveness/counter1.desc
@@ -1,7 +1,7 @@
 CORE
 counter1.sv
 --number-of-traces 2 --neural-liveness --neural-engine "echo Candidate: counter\\\\n"
-^\[main\.property\.p0\] always \(eventually main.counter == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter1.fail.desc b/regression/ebmc/ranking-function/counter1.fail.desc
index 277730e6c..d22743fc0 100644
--- a/regression/ebmc/ranking-function/counter1.fail.desc
+++ b/regression/ebmc/ranking-function/counter1.fail.desc
@@ -1,7 +1,7 @@
 CORE
 counter1.sv
 --ranking-function "(-counter)"
-^\[main\.property\.p0\] always \(eventually main.counter == 0\): INCONCLUSIVE$
+^\[main\.property\.p0\] always eventually main.counter == 0: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter1.pass.desc b/regression/ebmc/ranking-function/counter1.pass.desc
index 71263de08..fc37565a4 100644
--- a/regression/ebmc/ranking-function/counter1.pass.desc
+++ b/regression/ebmc/ranking-function/counter1.pass.desc
@@ -1,7 +1,7 @@
 CORE
 counter1.sv
 --ranking-function counter
-^\[main\.property\.p0\] always \(eventually main.counter == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter2.fail.desc b/regression/ebmc/ranking-function/counter2.fail.desc
index 383efa26c..e1a4e9a1e 100644
--- a/regression/ebmc/ranking-function/counter2.fail.desc
+++ b/regression/ebmc/ranking-function/counter2.fail.desc
@@ -1,7 +1,7 @@
 CORE
 counter2.sv
 --ranking-function counter
-^\[main\.property\.p0\] always \(eventually main.counter == 10\): INCONCLUSIVE$
+^\[main\.property\.p0\] always eventually main.counter == 10: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter2.pass.desc b/regression/ebmc/ranking-function/counter2.pass.desc
index 06abfdd09..ecf86dd28 100644
--- a/regression/ebmc/ranking-function/counter2.pass.desc
+++ b/regression/ebmc/ranking-function/counter2.pass.desc
@@ -1,7 +1,7 @@
 CORE
 counter2.sv
 --ranking-function 10-counter
-^\[main\.property\.p0\] always \(eventually main.counter == 10\): PROVED$
+^\[main\.property\.p0\] always eventually main.counter == 10: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter_in_module1.desc b/regression/ebmc/ranking-function/counter_in_module1.desc
index c1cb9947d..46c700ae2 100644
--- a/regression/ebmc/ranking-function/counter_in_module1.desc
+++ b/regression/ebmc/ranking-function/counter_in_module1.desc
@@ -1,7 +1,7 @@
 CORE
 counter_in_module1.sv
 --ranking-function instance.counter
-^\[main\.property\.p0\] always \(eventually main.instance.counter == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main.instance.counter == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter_with_reset1.fail.desc b/regression/ebmc/ranking-function/counter_with_reset1.fail.desc
index 76dc4a956..c87e0bb4f 100644
--- a/regression/ebmc/ranking-function/counter_with_reset1.fail.desc
+++ b/regression/ebmc/ranking-function/counter_with_reset1.fail.desc
@@ -1,7 +1,7 @@
 CORE
 counter_with_reset1.sv
 --property main.property.p0 --ranking-function 10-counter
-^\[main\.property\.p0\] always \(eventually main.counter == 10\): INCONCLUSIVE$
+^\[main\.property\.p0\] always eventually main.counter == 10: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/counter_with_reset1.pass.desc b/regression/ebmc/ranking-function/counter_with_reset1.pass.desc
index 199723552..bc3934194 100644
--- a/regression/ebmc/ranking-function/counter_with_reset1.pass.desc
+++ b/regression/ebmc/ranking-function/counter_with_reset1.pass.desc
@@ -1,7 +1,7 @@
 CORE
 counter_with_reset1.sv
 --property main.property.p1 --ranking-function 10-counter
-^\[main\.property\.p1\] always \(eventually main.reset \|\| main.counter == 10\): PROVED$
+^\[main\.property\.p1\] always eventually main.reset \|\| main.counter == 10: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc b/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc
index 09071e7df..32ddf6185 100644
--- a/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc
+++ b/regression/ebmc/ranking-function/lexicographic_ranking_function1.desc
@@ -1,7 +1,7 @@
 CORE
 lexicographic_ranking_function1.sv
 --ranking-function "{digit1, digit2}"
-^\[main\.property\.p0\] always \(eventually main\.digit1 == 0\): PROVED$
+^\[main\.property\.p0\] always eventually main\.digit1 == 0: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/verilog/system_verilog_assertion/eventually3.desc b/regression/verilog/system_verilog_assertion/eventually3.desc
index 73b6c6bec..ae76b4fac 100644
--- a/regression/verilog/system_verilog_assertion/eventually3.desc
+++ b/regression/verilog/system_verilog_assertion/eventually3.desc
@@ -3,6 +3,6 @@ eventually3.sv
 --module main --bound 11
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.property\.p0\] always \(eventually main\.counter <= 5\): REFUTED$
+^\[main\.property\.p0\] always eventually main\.counter <= 5: REFUTED$
 --
 ^warning: ignoring
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index d2e888949..159406793 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -386,9 +386,10 @@ std::string expr2verilogt::convert_sva(
 {
   if(src.operands().size()==1)
   {
+    auto &op = to_unary_expr(src).op();
     unsigned p;
-    auto s = convert(to_unary_expr(src).op(), p);
-    if(p == 0)
+    auto s = convert(op, p);
+    if(p == 0 && op.operands().size() >= 2)
       s = "(" + s + ")";
     return name + " " + s;
   }