mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix model converter in inliner. Bug reported by Sagar Chaki
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9d221c037a
commit
d6de73a2d1
|
@ -5668,7 +5668,8 @@ END_MLAPI_EXCLUDE
|
|||
Each conjunct encodes values of the bound variables of the query that are satisfied.
|
||||
In PDR mode, the returned answer is a single conjunction.
|
||||
|
||||
The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
|
||||
When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
|
||||
When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
|
||||
|
||||
def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
|
||||
*/
|
||||
|
|
|
@ -290,7 +290,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
TRACE("dl_dr",
|
||||
tout << r.get_decl()->get_name() << "\n";
|
||||
tout << mk_pp(r.get_head(), m) << " :- \n";
|
||||
for (unsigned i = 0; i < body.size(); ++i) {
|
||||
tout << mk_pp(body[i].get(), m) << "\n";
|
||||
});
|
||||
|
|
|
@ -423,6 +423,11 @@ namespace datalog {
|
|||
}
|
||||
|
||||
TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules; );
|
||||
|
||||
for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
|
||||
rule* r = m_inlined_rules.get_rule(i);
|
||||
datalog::del_rule(m_mc, *r);
|
||||
}
|
||||
}
|
||||
|
||||
bool mk_rule_inliner::transform_rule(rule_set const& orig, rule * r0, rule_set& tgt) {
|
||||
|
|
Loading…
Reference in a new issue