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;