mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

minor code simplifications

Browse source
This commit is contained in:
Nuno Lopes 2023-03-05 19:08:41 +00:00
parent 92fe8c5968
commit b9a87e493b
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/hoist_rewriter.cpp
View file

@ -37,7 +37,7 @@ expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) {
continue;
else
negs.push_back(::mk_not(m, a));
return expr_ref(::mk_not(m, mk_or(negs)), m);
return ::mk_not(mk_or(negs));
}
else
return ::mk_and(args);
@ -164,7 +164,6 @@ unsigned hoist_rewriter::mk_var(expr* e) {
}
expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsigned num_args, expr* const* es) {
expr_ref result(m);
expr_ref_vector args(m), args1(m), fmls(m);
for (unsigned i = 0; i < num_args; ++i) {
VERIFY(is_and(es[i], &args1));
@ -178,8 +177,7 @@ expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsi
fmls.push_back(mk_or(args));
for (auto* p : preds)
fmls.push_back(p);
result = mk_and(fmls);
return result;
return mk_and(fmls);
}