From a1f812dcbc0f139e66a938310324d3f3365af763 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 27 Feb 2015 12:15:47 +0000 Subject: 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. --- Source/Provers/SMTLib/SMTLibNamer.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/Provers') 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", "+", "-", "/", "*", "==", "<", ">", "<=", ">=", -- cgit v1.2.3