diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 2be19182a..e84646e7b 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -152,7 +152,6 @@ namespace arith {
         solver& a = dynamic_cast<solver&>(*s.fid2solver(fid));
         char const* name;
         expr_ref_vector args(m);
-        sort_ref_vector sorts(m);
 
         switch (m_ty) {
         case hint_type::farkas_h:
@@ -182,11 +181,6 @@ namespace arith {
             args.push_back(arith.mk_int(1));
             args.push_back(eq);
         }
-        for (expr* arg : args)
-            sorts.push_back(arg->get_sort());
-        sort* range = m.mk_proof_sort();
-        func_decl* d = m.mk_func_decl(symbol(name), args.size(), sorts.data(), range);
-        expr* r = m.mk_app(d, args);
-        return r;
+        return m.mk_app(symbol(name), args.size(), args.data(), m.mk_proof_sort());
     }
 }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 9528310d2..2aa46928b 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -674,7 +674,7 @@ namespace euf {
         }
 
         for (auto const& [e, v] : replay.m)
-            if (si.is_bool_op(e))
+            if (si.is_bool_op(e) && !si.is_cached(to_app(e), sat::literal(v, false)))
                si.cache(to_app(e), sat::literal(v, false));
         
         if (relevancy_enabled())
diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h
index e7d0d9b43..5fbf879ae 100644
--- a/src/sat/smt/sat_internalizer.h
+++ b/src/sat/smt/sat_internalizer.h
@@ -26,6 +26,7 @@ namespace sat {
         virtual literal internalize(expr* e, bool learned) = 0;
         virtual bool_var to_bool_var(expr* e) = 0;
         virtual bool_var add_bool_var(expr* e)  = 0;
+        virtual bool is_cached(app* t, literal l) const = 0;
         virtual void cache(app* t, literal l) = 0;
         virtual void uncache(literal l) = 0;
         virtual void push() = 0;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 038cd337b..a2d94652c 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -276,6 +276,13 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_lit2app.insert(l.index(), t);
         m_cache_trail.push_back(t);
     }
+
+    bool is_cached(app* t, sat::literal l) const override {
+        if (!m_app2lit.contains(t))
+            return false;
+        SASSERT(m_app2lit[t] == l);
+        return true;
+    }
     
     void convert_atom(expr * t, bool root, bool sign) {       
         SASSERT(m.is_bool(t));