diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp
index c200ccc49..64427aecd 100644
--- a/src/ast/rewriter/quant_hoist.cpp
+++ b/src/ast/rewriter/quant_hoist.cpp
@@ -214,12 +214,10 @@ private:
                     pull_quantifier(a->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
                     args.push_back(tmp);
                 }
-                if (rewrite_ok) {
-                m_rewriter.mk_and(args.size(), args.data(), result);
-            }
-                else {
+                if (rewrite_ok) 
+                    m_rewriter.mk_and(args.size(), args.data(), result);
+                else 
                     result = m.mk_and (args.size (), args.data ());
-                }
             }
             else if (m.is_or(fml)) {
                 num_args = to_app(fml)->get_num_args();
@@ -227,12 +225,10 @@ private:
                     pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp, use_fresh, rewrite_ok);
                     args.push_back(tmp);
                 }
-                if (rewrite_ok) {
-                m_rewriter.mk_or(args.size(), args.data(), result);
-            }
-                else {
+                if (rewrite_ok) 
+                    m_rewriter.mk_or(args.size(), args.data(), result);
+                else 
                     result = m.mk_or (args.size (), args.data ());
-                }
             }
             else if (m.is_not(fml)) {
                 pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp, use_fresh, rewrite_ok);
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 6a844a594..eef9ae77a 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -107,7 +107,7 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
                            mk_qe_lite_tactic(m, p),
                            cond(mk_has_quantifier_probe(), 
                                 cond(mk_is_lira_probe(),
-                                     mk_qsat_tactic(m, p),
+                                     or_else(mk_qsat_tactic(m, p), mk_smt_tactic(m)),
                                      mk_smt_tactic(m)),
                                 mk_smt_tactic(m)));
     st->updt_params(p);