Remove all references to bv2int (#800)

The `bv2nat` function is more standard now, working with CVC5, too.

Two of these references are just the Boogie-level name of functions, but
it’s nice to change those, too, so that there are no results when doing
`git grep bv2int`.

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",
       "+", "-", "/", "*", "==", "<", ">", "<=", ">=",

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

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