mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
e0393f85fa
commit
07e2ca100d
|
@ -718,7 +718,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
|
|||
op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT));
|
||||
op_names.push_back(builtin_name("bit2bool", OP_BIT2BOOL));
|
||||
|
||||
if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD") {
|
||||
if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD" || logic == "HORN") {
|
||||
op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL));
|
||||
op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL));
|
||||
op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));
|
||||
|
|
Loading…
Reference in a new issue