From 89c8f1722f33556def93aa54c92c3f2e3141014e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 12 Jul 2017 12:53:10 +0100 Subject: [PATCH] Fix typo that prevented uses of `bvsmod_i` being parsed. --- src/ast/bv_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 03b4fe637..321943c72 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I)); op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I)); op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I)); - op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I)); + op_names.push_back(builtin_name("bvsmod_i", OP_BSMOD_I)); op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT)); op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT));