mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 11:51:20 +00:00
Code Activity

fix bug reported by Nuno Lopes: inlining is unsound for negated predicates

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-01-02 17:37:35 -08:00
parent 81f1f7690d
commit 084a6f35eb
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -527,6 +527,9 @@ namespace datalog {
bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) { bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) {
if (r->has_negation()) {
return false;
}
SASSERT(rules.is_closed()); SASSERT(rules.is_closed());
const rule_stratifier& strat = rules.get_stratifier(); const rule_stratifier& strat = rules.get_stratifier();