ea

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jun 6, 2022 · dca1dcc · dca1dcc · NikolajBjorner · Jun 12, 2022
1 parent b629960
commit dca1dcc
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
@@ -80,7 +80,7 @@ namespace arith {
         if (m_nla) m_nla->collect_statistics(st);
     }
 
-    void solver::add_assumptions() {
+    void solver::explain_assumptions() {
         m_arith_hint.reset();
         unsigned i = 0;
         for (auto const & ev : m_explanation) {
@@ -119,7 +119,7 @@ namespace arith {
         if (!ctx.use_drat())
             return nullptr;
         m_arith_hint.m_ty = ty;
-        add_assumptions();
+        explain_assumptions();
         if (lit != sat::null_literal)
             m_arith_hint.m_literals.push_back({rational(1), ~lit});
         return &m_arith_hint;
@@ -129,7 +129,7 @@ namespace arith {
         if (!ctx.use_drat())
             return nullptr;
         m_arith_hint.m_ty = sat::hint_type::implied_eq_h;
-        add_assumptions();
+        explain_assumptions();
         m_arith_hint.m_diseqs.push_back({a->get_expr_id(), b->get_expr_id()});
         return &m_arith_hint;
     }

diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
@@ -423,7 +423,7 @@ namespace arith {
         sat::proof_hint m_farkas2;
         sat::proof_hint const* explain(sat::hint_type ty, sat::literal lit = sat::null_literal);
         sat::proof_hint const* explain_implied_eq(euf::enode* a, euf::enode* b);
-        void add_assumptions();
+        void explain_assumptions();
 
 
     public: