mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 09:05:31 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
4717d9d1f4
5 changed files with 268 additions and 43 deletions
|
@ -1104,10 +1104,10 @@ namespace datalog {
|
|||
|
||||
void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names){
|
||||
for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
|
||||
expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
|
||||
rules.push_back(r.get());
|
||||
// rules.push_back(m_rule_fmls[i].get());
|
||||
names.push_back(m_rule_names[i]);
|
||||
expr_ref r = bind_variables(m_rule_fmls[i].get(), true);
|
||||
rules.push_back(r.get());
|
||||
// rules.push_back(m_rule_fmls[i].get());
|
||||
names.push_back(m_rule_names[i]);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue