From f98e6a62fe62490f74d8abd77f3a51d541bf0207 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 03:49:48 -0700
Subject: [PATCH] fix #3648

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/tactic/smt_tactic.cpp | 1 +
 1 file changed, 1 insertion(+)

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()) {