From 16d34b9fcc2da4f6d62e1f719e0bb3cfc742c814 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Apr 2020 13:30:13 -0700
Subject: [PATCH] fix #4100

---
 src/sat/tactic/sat_tactic.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp
index 485384ae8..9b6d062d2 100644
--- a/src/sat/tactic/sat_tactic.cpp
+++ b/src/sat/tactic/sat_tactic.cpp
@@ -46,7 +46,6 @@ class sat_tactic : public tactic {
             bool produce_core = g->unsat_core_enabled();
             TRACE("before_sat_solver", g->display(tout););
             g->elim_redundancies();
-
             atom2bool_var map(m);
             obj_map<expr, sat::literal> dep2asm;
             sat::literal_vector assumptions;
@@ -113,6 +112,10 @@ class sat_tactic : public tactic {
                 ref<sat2goal::mc> mc;
                 m_sat2goal(*m_solver, map, m_params, *(g.get()), mc);
                 g->add(mc.get());
+                if (produce_core) {
+                    // sat2goal does not preseve assumptions
+                    g->updt_prec(goal::OVER);
+                }
             }
             g->inc_depth();
             result.push_back(g.get());