Merge remote-tracking branch 'upstream/master' into reproducible-reso…

…urce-limit
boogie-org · Oct 17, 2023 · 446c942 · 446c942
2 parents 05db7d3 + 3bbffe3
commit 446c942
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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) }