From 3bbffe3ce383a8f820af823a33f53e5e72610c80 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 17 Oct 2023 01:02:22 -0700 Subject: [PATCH] Remove all references to `bv2int` (#800) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 2 +- Test/smack/git-issue-203-define.bpl | 2 +- Test/smack/git-issue-203.bpl | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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) }