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

Fix typo that prevented uses of bvsmod_i being parsed.

This commit is contained in:
Dan Liew 2017-07-12 12:53:10 +01:00
parent bf83b897a1
commit 89c8f1722f

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));