summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers')
-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",
"+", "-", "/", "*", "==", "<", ">", "<=", ">=",