fix #6623

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);

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;

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