diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-27 12:15:47 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-27 12:15:47 +0000 |
| commit | a1f812dcbc0f139e66a938310324d3f3365af763 (patch) | |
| tree | c3ea745191e803ebd0bd3716d32b4d9babbadb13 /Source | |
| parent | 7cd4f74474c3935e6d0e67d67e86c6c8326a95a4 (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.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 2 |
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",
"+", "-", "/", "*", "==", "<", ">", "<=", ">=",
|