mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Disable FPA-min/max because of name clashes with user-defined functions.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-10-18 13:43:13 +01:00
parent fe4a8b44a5
commit f4a015602c
1 changed files with 3 additions and 2 deletions

5
src/ast/float_decl_plugin.cpp
View file

@ -581,8 +581,9 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
// Disabled min/max, clashes with user-defined min/max functions
// op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
// op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));