From 42d30e3eddcfff602da327db907fe3dc699c78d5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Jul 2018 08:20:14 -0700 Subject: [PATCH] remove availability of divides as it clashes with user-defined functions in benchmarks Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 3c5e2e1c0..db3604a99 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -549,7 +549,8 @@ void arith_decl_plugin::get_op_names(svector& 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));