diff --git a/regression/ebmc/smv-netlist/s_until1.desc b/regression/ebmc/smv-netlist/s_until1.desc
index 4d59d8c20..b491f34dc 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 \(1\) 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 134f7b97c..61244e9d0 100644
--- a/src/trans-netlist/smv_netlist.cpp
+++ b/src/trans-netlist/smv_netlist.cpp
@@ -51,12 +51,12 @@ void print_smv(const netlistt &netlist, std::ostream &out, literalt a)
 {
   if(a == const_literal(false))
   {
-    out << "0";
+    out << "FALSE";
     return;
   }
   else if(a == const_literal(true))
   {
-    out << "1";
+    out << "TRUE";
     return;
   }