mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

remove availability of divides as it clashes with user-defined functions in benchmarks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-31 08:20:14 -07:00
parent f22f415133
commit 42d30e3edd
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/arith_decl_plugin.cpp
View file

@ -549,7 +549,8 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("*",OP_MUL));
op_names.push_back(builtin_name("/",OP_DIV));
op_names.push_back(builtin_name("div",OP_IDIV));
op_names.push_back(builtin_name("divides",OP_IDIVIDES));
// clashes with user-defined functions
// op_names.push_back(builtin_name("divides",OP_IDIVIDES));
op_names.push_back(builtin_name("rem",OP_REM));
op_names.push_back(builtin_name("mod",OP_MOD));
op_names.push_back(builtin_name("to_real",OP_TO_REAL));