diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index 4418f0f9f..472f6b30c 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -56,8 +56,6 @@ class fpa2bv_tactic : public tactic {
                                 proof_converter_ref & pc,
                                 expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
-            fail_if_proof_generation("fpa2bv", g);
-            fail_if_unsat_core_generation("fpa2bv", g);
             m_proofs_enabled      = g->proofs_enabled();
             m_produce_models      = g->models_enabled();
             m_produce_unsat_cores = g->unsat_core_enabled();
diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp
index 485e837ee..9c94d6cb2 100644
--- a/src/tactic/fpa/qffp_tactic.cpp
+++ b/src/tactic/fpa/qffp_tactic.cpp
@@ -71,21 +71,19 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
 
     tactic * st = and_then(mk_simplify_tactic(m, simp_p),
                            mk_propagate_values_tactic(m, p),
-                           cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
-                                mk_smt_tactic(),
-                                and_then(
-                                     mk_fpa2bv_tactic(m, p),
-                                     mk_propagate_values_tactic(m, p),
-                                     using_params(mk_simplify_tactic(m, p), simp_p),                                 
-                                     mk_bit_blaster_tactic(m, p),
-                                     using_params(mk_simplify_tactic(m, p), simp_p),
-                                     cond(mk_is_propositional_probe(),
-                                        mk_sat_tactic(m, p),
-                                        cond(mk_has_fp_to_real_probe(),
-                                            mk_qfnra_tactic(m, p),
-                                            mk_smt_tactic(p))
-                                        ),
-                                     mk_fail_if_undecided_tactic())));
+                           mk_fpa2bv_tactic(m, p),
+                           mk_propagate_values_tactic(m, p),
+                           using_params(mk_simplify_tactic(m, p), simp_p),
+                           mk_bit_blaster_tactic(m, p),
+                           using_params(mk_simplify_tactic(m, p), simp_p),
+                           cond(mk_is_propositional_probe(),
+                                cond(mk_produce_proofs_probe(),
+                                     mk_smt_tactic(), // `sat' does not support proofs.
+                                     mk_sat_tactic(m, p)),
+                                cond(mk_has_fp_to_real_probe(),
+                                     mk_qfnra_tactic(m, p),
+                                     mk_smt_tactic(p))),
+                            mk_fail_if_undecided_tactic());
 
     st->updt_params(p);
     return st;