mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
minor code simplification
This commit is contained in:
parent
8981d32caf
commit
ca6fed8b25
|
@ -2444,8 +2444,7 @@ namespace {
|
||||||
}
|
}
|
||||||
|
|
||||||
tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
|
tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
|
||||||
return alloc(dependent_expr_state_tactic, m, p,
|
return alloc(dependent_expr_state_tactic, m, p, mk_qe_lite_simplifer);
|
||||||
[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(qe_lite_simplifier, m, p, s); });
|
|
||||||
}
|
}
|
||||||
|
|
||||||
dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
|
dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
|
||||||
|
|
Loading…
Reference in a new issue