3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Merge pull request #1144 from delcypher/fix_parse_bvsmod_i

Fix typo that prevented uses of `bvsmod_i` being parsed.
This commit is contained in:
Christoph M. Wintersteiger 2017-07-12 15:47:24 +01:00 committed by GitHub
commit baedf41c6c

View file

@ -732,7 +732,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & 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));