Merge pull request #1394 from diffblue/smv-TRUE-paren

SMV netlist: avoid parentheses around TRUE

Author: tautschnig

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$
 --

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()};