diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 9b0f8d617..a2a7f2a32 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -269,6 +269,7 @@ public:
                 if (pr) {
                     in->reset();
                     in->assert_expr(m.get_fact(pr), pr, nullptr);
+                    in->updt_prec(goal::UNDER_OVER);
                 }
                 if (m_candidate_models) {
                     switch (m_ctx->last_failure()) {