mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix unhandled finite domain sort rewrite case. Issue #918
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
996c0f0666
commit
899843b7cd
|
@ -64,7 +64,10 @@ class dt2bv_tactic : public tactic {
|
|||
return;
|
||||
}
|
||||
|
||||
if (m_t.is_fd(a)) {
|
||||
if (m_t.is_fd(a) && a->get_num_args() > 0) {
|
||||
m_t.m_non_fd_sorts.insert(get_sort(a));
|
||||
}
|
||||
else if (m_t.is_fd(a)) {
|
||||
m_t.m_fd_sorts.insert(get_sort(a));
|
||||
}
|
||||
else {
|
||||
|
|
Loading…
Reference in a new issue