SMV: do not use parentheses around nullary operands of !

This changes the special-casing for adding parentheses around the operand of
boolean negation. There is no need for parentheses around nullary operands.

Author: kroening

regression/ebmc/smv-word-level/smv1.desc

@@ -10,7 +10,7 @@ smv1.smv
 ^INIT range_type = 1$
 ^INIT signed_bit_vector = 0sd20_1$
 ^INIT unsigned_bit_vector = 0ud20_1$
-^TRANS next\(bool_type\) = \(!\(bool_type\)\)$
+^TRANS next\(bool_type\) = \(!bool_type\)$
 ^TRANS next\(range_type\) = 2$
 ^TRANS next\(signed_bit_vector\) = 0sd20_2$
 ^TRANS next\(unsigned_bit_vector\) = 0ud20_2$

src/smvlang/expr2smv.cpp

@@ -419,7 +419,7 @@ expr2smvt::resultt expr2smvt::convert_unary(
   // clang-format off
   bool parentheses =
       op.operands().size() == 1 ? false
-    : src.id() == ID_not        ? true
+    : src.id() == ID_not && !op.operands().empty() ? true
     : precedence >= op_rec.p;
   // clang-format on