mirror of
https://github.com/Z3Prover/z3
synced 2025-08-31 07:14:54 +00:00
fix build
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d50fc6976b
commit
f986ae97bd
5 changed files with 12 additions and 12 deletions
|
@ -335,7 +335,7 @@ namespace datalog {
|
|||
rule_set * mk_subsumption_checker::operator()(rule_set const & source) {
|
||||
// TODO mc
|
||||
if (!m_context.get_params ().xform_subsumption_checker())
|
||||
return nullptr;
|
||||
return nullptr;
|
||||
|
||||
m_have_new_total_rule = false;
|
||||
collect_ground_unconditional_rule_heads(source);
|
||||
|
@ -356,8 +356,7 @@ namespace datalog {
|
|||
SASSERT(m_new_total_relation_discovery_during_transformation || !m_have_new_total_rule);
|
||||
while (m_have_new_total_rule) {
|
||||
m_have_new_total_rule = false;
|
||||
|
||||
scoped_ptr<rule_set> old = res;
|
||||
scoped_ptr<rule_set> old = res.detach();
|
||||
res = alloc(rule_set, m_context);
|
||||
transform_rules(*old, *res);
|
||||
}
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue