From 29969648ba7b2f567b5b35ae2330cae5a4803454 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Mar 2017 05:52:46 +0100 Subject: [PATCH] check that formulas are in lira before invoking qsat. Issue #919 Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/quant_tactics.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 044511c33..7d428b369 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -28,6 +28,7 @@ Revision History: #include"ctx_simplify_tactic.h" #include"smt_tactic.h" #include"elim_term_ite_tactic.h" +#include"probe_arith.h" static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) { 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), mk_qe_lite_tactic(m, p), cond(mk_has_quantifier_probe(), - or_else(mk_qsat_tactic(m, p), - and_then(mk_qe_tactic(m), mk_smt_tactic())), + cond(mk_is_lira_probe(), + or_else(mk_qsat_tactic(m, p), + and_then(mk_qe_tactic(m), mk_smt_tactic())), + mk_smt_tactic()), mk_smt_tactic())); st->updt_params(p); return st;