mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
parent
b4e7730034
commit
d3db2af81d
|
@ -569,6 +569,7 @@ namespace datalog {
|
|||
|
||||
void context::check_rules(rule_set& r) {
|
||||
m_rule_properties.set_generate_proof(generate_proof_trace());
|
||||
TRACE("dl", m_rule_set.display(tout););
|
||||
switch(get_engine()) {
|
||||
case DATALOG_ENGINE:
|
||||
m_rule_properties.collect(r);
|
||||
|
|
|
@ -257,7 +257,6 @@ void rule_properties::reset() {
|
|||
m_negative_rules.reset();
|
||||
m_inf_sort.reset();
|
||||
m_collected = false;
|
||||
m_is_monotone = true;
|
||||
m_generate_proof = false;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue