mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add missing interpreted tail during bottom-up simplification #1452
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1992749e78
commit
5159291d57
|
@ -79,6 +79,10 @@ namespace datalog {
|
|||
}
|
||||
if (contained) {
|
||||
if (new_tail) {
|
||||
for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i) {
|
||||
m_new_tail.push_back(r->get_tail(i));
|
||||
m_new_tail_neg.push_back(false);
|
||||
}
|
||||
rule* new_r = m_context.get_rule_manager().mk(r->get_head(), m_new_tail.size(),
|
||||
m_new_tail.c_ptr(), m_new_tail_neg.c_ptr(), symbol::null, false);
|
||||
res->add_rule(new_r);
|
||||
|
|
Loading…
Reference in a new issue