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

check that formulas are in lira before invoking qsat. Issue #919

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-09 05:52:46 +01:00
parent fcda4cee9f
commit 29969648ba
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -28,6 +28,7 @@ Revision History:
#include"ctx_simplify_tactic.h" #include"ctx_simplify_tactic.h"
#include"smt_tactic.h" #include"smt_tactic.h"
#include"elim_term_ite_tactic.h" #include"elim_term_ite_tactic.h"
#include"probe_arith.h"
static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) { static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
params_ref pull_ite_p; params_ref pull_ite_p;
@ -107,8 +108,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
tactic * st = and_then(mk_quant_preprocessor(m), tactic * st = and_then(mk_quant_preprocessor(m),
mk_qe_lite_tactic(m, p), mk_qe_lite_tactic(m, p),
cond(mk_has_quantifier_probe(), cond(mk_has_quantifier_probe(),
or_else(mk_qsat_tactic(m, p), cond(mk_is_lira_probe(),
and_then(mk_qe_tactic(m), mk_smt_tactic())), or_else(mk_qsat_tactic(m, p),
and_then(mk_qe_tactic(m), mk_smt_tactic())),
mk_smt_tactic()),
mk_smt_tactic())); mk_smt_tactic()));
st->updt_params(p); st->updt_params(p);
return st; return st;