Merge pull request #1383 from diffblue/smv-bitnot

SMV: bitwise negation operator

Author: tautschnig

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

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)

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