mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
add call to function
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f74adb1ebd
commit
e5c5caea45
|
@ -417,7 +417,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
|
||||||
match(*m_sigs[k], arity, domain, range, rng);
|
match(*m_sigs[k], arity, domain, range, rng);
|
||||||
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
|
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
|
||||||
case OP_STRING_UBVTOS:
|
case OP_STRING_UBVTOS:
|
||||||
NOT_IMPLEMENTED_YET();
|
return mk_ubv2s(arity, domain);
|
||||||
|
|
||||||
case _OP_REGEXP_FULL_CHAR:
|
case _OP_REGEXP_FULL_CHAR:
|
||||||
m_has_re = true;
|
m_has_re = true;
|
||||||
|
|
Loading…
Reference in a new issue