mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
dc0887db5a
commit
241e845da8
|
@ -370,7 +370,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
|
|||
if (is_real) {
|
||||
return m_manager->mk_func_decl(symbol("^0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0));
|
||||
}
|
||||
return m_manager->mk_func_decl(symbol("^0"), m_int_decl, m_int_decl, m_int_decl, func_decl_info(m_family_id, OP_POWER0));
|
||||
return m_manager->mk_func_decl(symbol("^0"), m_int_decl, m_int_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0));
|
||||
case OP_TO_REAL: return m_to_real_decl;
|
||||
case OP_TO_INT: return m_to_int_decl;
|
||||
case OP_IS_INT: return m_is_int_decl;
|
||||
|
@ -834,7 +834,7 @@ bool arith_util::is_considered_uninterpreted(func_decl* f, unsigned n, expr* con
|
|||
func_decl* arith_util::mk_ipower0() {
|
||||
sort* s = mk_int();
|
||||
sort* rs[2] = { s, s };
|
||||
return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, s);
|
||||
return m_manager.mk_func_decl(arith_family_id, OP_POWER0, 0, nullptr, 2, rs, mk_real());
|
||||
}
|
||||
|
||||
func_decl* arith_util::mk_rpower0() {
|
||||
|
|
Loading…
Reference in a new issue