From 4a142b0f81c16b3e60972a112233d21ee909c540 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 9 Apr 2023 21:10:24 -0700
Subject: [PATCH] fix #6623

---
 src/sat/smt/pb_internalize.cpp |  5 +++++
 src/sat/smt/sat_internalizer.h |  1 +
 src/sat/tactic/goal2sat.cpp    | 13 +++++++++----
 3 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp
index 17f2bd4ded6..abbd79c44d2 100644
--- a/src/sat/smt/pb_internalize.cpp
+++ b/src/sat/smt/pb_internalize.cpp
@@ -41,6 +41,11 @@ namespace pb {
         SASSERT(m_pb.is_pb(e));
         app* t = to_app(e);
         rational k = m_pb.get_k(t);
+        if (!root && is_app(e)) {
+            sat::literal lit = si.get_cached(to_app(e));
+            if (lit != sat::null_literal)
+                return sign ? ~lit : lit;
+        }
         switch (t->get_decl_kind()) {
         case OP_AT_MOST_K:
             return convert_at_most_k(t, k, root, sign);
diff --git a/src/sat/smt/sat_internalizer.h b/src/sat/smt/sat_internalizer.h
index 5be20c4e0ee..7b1d932eca3 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) = 0;
         virtual bool_var to_bool_var(expr* e) = 0;
         virtual bool_var add_bool_var(expr* e)  = 0;
+        virtual literal get_cached(app* t) const = 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;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index c107a74c500..2678888044c 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -276,11 +276,16 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_cache_trail.push_back(t);
     }
 
+    sat::literal get_cached(app* t) const override {
+        sat::literal lit = sat::null_literal;
+        m_app2lit.find(t, lit);
+        return lit;
+    }
+
     bool is_cached(app* t, sat::literal l) const override {
-        if (!m_app2lit.contains(t))
-            return false;
-        SASSERT(m_app2lit[t] == l);
-        return true;
+        sat::literal lit = get_cached(t);
+        SASSERT(lit == sat::null_literal || l == lit);
+        return l == lit;
     }
     
     void convert_atom(expr * t, bool root, bool sign) {