mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #5002

Browse source 
Avoid code path that uses qe_tactic as it isn't protected against parameter abuse
This commit is contained in:
Nikolaj Bjorner 2021-02-12 13:20:51 -08:00
parent 80d297dca2
commit 4991c6c2c6
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/smtlogics/quant_tactics.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include "tactic/core/propagate_values_tactic.h" #include "tactic/core/propagate_values_tactic.h"
#include "tactic/core/solve_eqs_tactic.h" #include "tactic/core/solve_eqs_tactic.h"
#include "tactic/core/elim_uncnstr_tactic.h" #include "tactic/core/elim_uncnstr_tactic.h"
#include "qe/qe_tactic.h"
#include "qe/qe_lite.h" #include "qe/qe_lite.h"
#include "qe/qsat.h" #include "qe/qsat.h"
#include "tactic/core/ctx_simplify_tactic.h" #include "tactic/core/ctx_simplify_tactic.h"
@ -108,8 +107,7 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
mk_qe_lite_tactic(m, p), mk_qe_lite_tactic(m, p),
cond(mk_has_quantifier_probe(), cond(mk_has_quantifier_probe(),
cond(mk_is_lira_probe(), cond(mk_is_lira_probe(),
or_else(mk_qsat_tactic(m, p), mk_qsat_tactic(m, p),
and_then(mk_qe_tactic(m), mk_smt_tactic(m))),
mk_smt_tactic(m)), mk_smt_tactic(m)),
mk_smt_tactic(m))); mk_smt_tactic(m)));
st->updt_params(p); st->updt_params(p);