From 2e714fca7c334bf63e18e5e18daa1cf8f5b339fa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 May 2020 13:53:10 -0700 Subject: [PATCH] expose uninterpreted op versions for ad-hoc parsing --- src/ast/arith_decl_plugin.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index aa36acc6a0a..3bcaf10b513 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -608,6 +608,10 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("atanh", OP_ATANH)); op_names.push_back(builtin_name("pi", OP_PI)); op_names.push_back(builtin_name("euler", OP_E)); + op_names.push_back(builtin_name("/0",OP_DIV0)); + op_names.push_back(builtin_name("div0",OP_IDIV0)); + op_names.push_back(builtin_name("rem0",OP_REM0)); + op_names.push_back(builtin_name("mod0",OP_MOD0)); } }