diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 7df4a2b64..30665c6e5 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -955,11 +955,11 @@ namespace pdr {
        and predicates that are satisfied from facts to the query.
        The resulting trace 
      */
-
     expr_ref model_search::get_trace(context const& ctx) const {       
         pred_transformer& pt = get_root().pt();
         ast_manager& m = pt.get_manager();
         manager& pm = pt.get_pdr_manager();
+
         datalog::context& dctx = ctx.get_context();
         datalog::rule_manager& rm = dctx.get_rule_manager();
         expr_ref_vector constraints(m), predicates(m);
diff --git a/src/muz_qe/qe_sat_tactic.h b/src/muz_qe/qe_sat_tactic.h
index c539216be..15228c534 100644
--- a/src/muz_qe/qe_sat_tactic.h
+++ b/src/muz_qe/qe_sat_tactic.h
@@ -26,7 +26,7 @@ Revision History:
 
 namespace qe {
         
-    tactic * mk_sat_tactic(ast_manager& m, params_ref const& p);
+    tactic * mk_sat_tactic(ast_manager& m, params_ref const& p = params_ref());
     
 };
 /*
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 85f53eff0..937b0229e 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include"solve_eqs_tactic.h"
 #include"elim_uncnstr_tactic.h"
 #include"qe_tactic.h"
+#include"qe_sat_tactic.h"
 #include"ctx_simplify_tactic.h"
 #include"smt_tactic.h"
 
@@ -98,8 +99,11 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
 
 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = and_then(mk_quant_preprocessor(m),
-                           mk_qe_tactic(m),
-                           mk_smt_tactic());
+                           or_else(try_for(mk_smt_tactic(), 100), 
+                                   try_for(qe::mk_sat_tactic(m), 1000), 
+                                   try_for(mk_smt_tactic(), 1000),
+                                   and_then(mk_qe_tactic(m), mk_smt_tactic())));
+
     st->updt_params(p);
     return st;
 }