summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-27 12:15:47 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-27 12:15:47 +0000
commita1f812dcbc0f139e66a938310324d3f3365af763 (patch)
treec3ea745191e803ebd0bd3716d32b4d9babbadb13
parent7cd4f74474c3935e6d0e67d67e86c6c8326a95a4 (diff)
Fix using "mkbv" as a variable name in a boogie program. This was
taken from ``bv_decl_plugin::get_op_names(...)`` in ``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code.
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index 8e000403..3ef2039b 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -37,7 +37,7 @@ namespace Microsoft.Boogie.SMTLib
"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",
+ "rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int", "mkbv",
// floating point (FIXME: Legacy, remove this)
"plusInfinity", "minusInfinity",
"+", "-", "/", "*", "==", "<", ">", "<=", ">=",