diff --git a/regression/smv/word/bitwise1.desc b/regression/smv/word/bitwise1.desc
index ae7184773..cba35572a 100644
--- a/regression/smv/word/bitwise1.desc
+++ b/regression/smv/word/bitwise1.desc
@@ -1,8 +1,8 @@
 CORE
 bitwise1.smv
 
-^\[.*\] !\(0ud8_123 = 0ud8_132\): PROVED .*$
-^\[.*\] !\(0sd8_123 = -0sd8_124\): PROVED .*$
+^\[.*\] \(!0ud8_123\) = 0ud8_132: PROVED .*$
+^\[.*\] \(!0sd8_123\) = -0sd8_124: PROVED .*$
 ^\[.*\] \(0ud8_123 \& 0ud8_7\) = 0ud8_3: PROVED .*$
 ^\[.*\] \(0ud8_123 \| 0ud8_7\) = 0ud8_127: PROVED .*$
 ^\[.*\] \(0ud8_123 xor 0ud8_7\) = 0ud8_124: PROVED .*$
diff --git a/regression/smv/word/bitwise1.smv b/regression/smv/word/bitwise1.smv
index 4d2884b73..d80dbc400 100644
--- a/regression/smv/word/bitwise1.smv
+++ b/regression/smv/word/bitwise1.smv
@@ -1,8 +1,8 @@
 MODULE main
 
 -- negation
-SPEC !uwconst(123, 8) = uwconst(132, 8)
-SPEC !swconst(123, 8) = swconst(-124, 8)
+SPEC (!uwconst(123, 8)) = uwconst(132, 8)
+SPEC (!swconst(123, 8)) = swconst(-124, 8)
 
 -- and
 SPEC (uwconst(123, 8) & uwconst(7, 8)) = uwconst(3, 8)
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index c525c5818..c03be94e8 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -771,8 +771,8 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
   else if(src.id()==ID_notequal)
     return convert_binary(to_notequal_expr(src), "!=", precedencet::REL);
 
-  else if(src.id()==ID_not)
-    return convert_unary(to_not_expr(src), "!", precedencet::NOT);
+  else if(src.id() == ID_not || src.id() == ID_bitnot)
+    return convert_unary(to_unary_expr(src), "!", precedencet::NOT);
 
   else if(src.id() == ID_and || src.id() == ID_bitand)
     return convert_binary_associative(src, "&", precedencet::AND);