mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
fix #6082
This commit is contained in:
parent
352666b19f
commit
56aa4261b6
|
@ -36,7 +36,7 @@ namespace smt {
|
|||
if (!m_next) {
|
||||
sort* s = decl()->get_domain(0);
|
||||
sort* domain[2] = {s, s};
|
||||
m_next = m.mk_fresh_func_decl("next", "", 2, domain, s);
|
||||
m_next = m.mk_fresh_func_decl("specrel.next", "", 2, domain, s, false);
|
||||
}
|
||||
return m_next;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue