diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index b3a6e77ff4d..00564ed3e95 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -811,6 +811,7 @@ namespace smt {
         init_bits(e, bits);                                                                
     }
 
+    MK_UNARY(internalize_neg,       mk_neg);
     MK_UNARY(internalize_not,       mk_not);
     MK_UNARY(internalize_redand,    mk_redand);
     MK_UNARY(internalize_redor,     mk_redor);
@@ -895,6 +896,7 @@ namespace smt {
         }
         switch (term->get_decl_kind()) {
         case OP_BV_NUM:         internalize_num(term); return true;
+        case OP_BNEG:           internalize_neg(term); return true;
         case OP_BADD:           internalize_add(term); return true;
         case OP_BSUB:           internalize_sub(term); return true;
         case OP_BMUL:           internalize_mul(term); return true;
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 588f19d89cb..73d659c688c 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -196,6 +196,7 @@ namespace smt {
         void internalize_ext_rotate_right(app * n);
         void internalize_and(app * n);
         void internalize_or(app * n);
+        void internalize_neg(app * n);
         void internalize_not(app * n);
         void internalize_nand(app * n);
         void internalize_nor(app * n);