diff --git a/regression/ebmc/smv-netlist/s_until1.desc b/regression/ebmc/smv-netlist/s_until1.desc
index b491f34dc..a0691d38e 100644
--- a/regression/ebmc/smv-netlist/s_until1.desc
+++ b/regression/ebmc/smv-netlist/s_until1.desc
@@ -2,7 +2,7 @@ CORE
 s_until1.sv
 --smv-netlist
 ^LTLSPEC \(\!node144\) U node151$
-^LTLSPEC \(TRUE\) U node158$
+^LTLSPEC TRUE U node158$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/trans-netlist/smv_netlist.cpp b/src/trans-netlist/smv_netlist.cpp
index 61244e9d0..c321fcb37 100644
--- a/src/trans-netlist/smv_netlist.cpp
+++ b/src/trans-netlist/smv_netlist.cpp
@@ -106,7 +106,7 @@ void print_smv(const netlistt &netlist, std::ostream &out, const exprt &expr)
         std::ostringstream buffer;
         auto l = to_literal_expr(expr).get_literal();
         print_smv(netlist, buffer, l);
-        if(l.sign())
+        if(l.sign() && !l.is_constant())
           return {precedencet::NOT, buffer.str()};
         else
           return {precedencet::MAX, buffer.str()};