diff --git a/Source/Provers/SMTLib/SmtLibNameUtils.cs b/Source/Provers/SMTLib/SmtLibNameUtils.cs
index f768a6198..30304dc6c 100644
--- a/Source/Provers/SMTLib/SmtLibNameUtils.cs
+++ b/Source/Provers/SMTLib/SmtLibNameUtils.cs
@@ -41,7 +41,7 @@ public static string QuoteId(string s)
       "bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge",
       "bvsge", "bvslt", "bvugt", "bvsgt", "bvxor", "bvnand", "bvnor", "bvxnor", "sign_extend", "zero_extend",
       "repeat", "bvredor", "bvredand", "bvcomp", "bvumul_noovfl", "bvsmul_noovfl", "bvsmul_noudfl", "bvashr",
-      "rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int", "mkbv",
+      "rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2nat", "mkbv",
       // floating point (FIXME: Legacy, remove this)
       "plusInfinity", "minusInfinity",
       "+", "-", "/", "*", "==", "<", ">", "<=", ">=",
diff --git a/Test/smack/git-issue-203-define.bpl b/Test/smack/git-issue-203-define.bpl
index 96696f95e..1310d8fd8 100644
--- a/Test/smack/git-issue-203-define.bpl
+++ b/Test/smack/git-issue-203-define.bpl
@@ -54,7 +54,7 @@ function {:define} $isExternal(p: ref) returns (bool) { $slt.ref.bool(p, $EXTERN
 
 // SMT bit-vector/integer conversion
 function {:builtin "(_ int2bv 64)"} $int2bv.64(i: i64) returns (bv64);
-function {:builtin "bv2nat"} $bv2int.64(i: bv64) returns (i64);
+function {:builtin "bv2nat"} $bv2nat.64(i: bv64) returns (i64);
 
 // Integer arithmetic operations
 function {:define} $add.i1(i1: i1, i2: i1) returns (i1) { (i1 + i2) }
diff --git a/Test/smack/git-issue-203.bpl b/Test/smack/git-issue-203.bpl
index df27570b9..319540032 100644
--- a/Test/smack/git-issue-203.bpl
+++ b/Test/smack/git-issue-203.bpl
@@ -54,7 +54,7 @@ function {:inline} $isExternal(p: ref) returns (bool) { $slt.ref.bool(p, $EXTERN
 
 // SMT bit-vector/integer conversion
 function {:builtin "(_ int2bv 64)"} $int2bv.64(i: i64) returns (bv64);
-function {:builtin "bv2nat"} $bv2int.64(i: bv64) returns (i64);
+function {:builtin "bv2nat"} $bv2nat.64(i: bv64) returns (i64);
 
 // Integer arithmetic operations
 function {:inline} $add.i1(i1: i1, i2: i1) returns (i1) { (i1 + i2) }