From 0b2bf3f587ab0335fe852c208b7fcc54c340c290 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 14:53:14 +0200 Subject: [PATCH] Add friend class declaration for testing --- src/smt/theory_finite_set.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 38480ba87..59a8651a7 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -92,6 +92,7 @@ theory_finite_set.cpp. namespace smt { class theory_finite_set : public theory { + friend class theory_finite_set_test; finite_set_util u; finite_set_axioms m_axioms; obj_hashtable m_elements; // set of all 'x' where there is an 'x in S' atom @@ -114,6 +115,9 @@ namespace smt { // Helper methods for axiom instantiation void instantiate_axioms(expr* elem, expr* set); void add_clause(expr_ref_vector const& clause); + void instantiate_false_lemma(); + void instantiate_unit_propagation(); + void instantiate_free_lemma(); public: theory_finite_set(context& ctx);