diff --git a/src/main/scala/leon/genc/CConverter.scala b/src/main/scala/leon/genc/CConverter.scala
index e1b4a47909a96454a63321825a923bd571ed9330..d8a52687c353a5f0aac4d64b9230719b516c240f 100644
--- a/src/main/scala/leon/genc/CConverter.scala
+++ b/src/main/scala/leon/genc/CConverter.scala
@@ -337,7 +337,7 @@ class CConverter(val ctx: LeonContext, val prog: Program) {
     case BVTimes(lhs, rhs)        => buildBinOp(lhs, "*",   rhs)
     case BVDivision(lhs, rhs)     => buildBinOp(lhs, "/",   rhs)
     case BVRemainder(lhs, rhs)    => buildBinOp(lhs, "%",   rhs)
-    case BVNot(rhs)               => buildUnOp (     "!",   rhs) // TODO check if this one isn't in fact '~'
+    case BVNot(rhs)               => buildUnOp (     "~",   rhs)
     case BVAnd(lhs, rhs)          => buildBinOp(lhs, "&",   rhs)
     case BVOr(lhs, rhs)           => buildBinOp(lhs, "|",   rhs)
     case BVXOr(lhs, rhs)          => buildBinOp(lhs, "^",   rhs)
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 7bebde2f800965d26eae30befc00f92512cf72e0..f2be95fb0ca9c8c9185c462414635060689fccba 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -164,6 +164,7 @@ class PrettyPrinter(opts: PrinterOptions,
       case Or(exprs)            => optP { p"${nary(exprs, "| || ")}" } // Ugliness award! The first | is there to shield from stripMargin()
       case Not(Equals(l, r))    => optP { p"$l \u2260 $r" }
       case Implies(l,r)         => optP { p"$l ==> $r" }
+      case BVNot(expr)          => p"~$expr"
       case UMinus(expr)         => p"-$expr"
       case BVUMinus(expr)       => p"-$expr"
       case RealUMinus(expr)     => p"-$expr"