fixes to #7250

src/ast/euf/euf_egraph.cpp

@@ -231,7 +231,7 @@ namespace euf {
             for (auto const& q : euf::enode_th_vars(r2))
                 if (p.get_id() == q.get_id()) 
                     add_th_diseq(p.get_id(), p.get_var(), q.get_var(), n);
-    }
+        }
     }
 
 

src/sat/smt/bv_solver.cpp

@@ -301,6 +301,28 @@ namespace bv {
     bool solver::is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) { return false; }
     bool solver::is_external(bool_var v) { return true; }
 
+    euf::enode_pair solver::get_justification_eq(size_t j) {
+        auto& c = bv_justification::from_index(j);
+        TRACE("bv", display_constraint(tout, j) << "\n";);
+        switch (c.m_kind) {
+        case bv_justification::kind_t::eq2bit:
+            UNREACHABLE();
+            return euf::enode_pair();
+        case bv_justification::kind_t::ne2bit: 
+            UNREACHABLE();
+            return euf::enode_pair();        
+        case bv_justification::kind_t::bit2eq: 
+            return { var2enode(c.m_v1), var2enode(c.m_v2) };        
+        case bv_justification::kind_t::bit2ne: 
+            UNREACHABLE();
+            return euf::enode_pair();
+        case bv_justification::kind_t::bv2int: 
+            UNREACHABLE();
+            return euf::enode_pair();        
+        }
+        return euf::enode_pair();
+    }
+
     void solver::get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector& r, bool probing) {
         auto& c = bv_justification::from_index(idx);
         TRACE("bv", display_constraint(tout, idx) << "\n";);

src/sat/smt/bv_solver.h

@@ -349,6 +349,7 @@ namespace bv {
         bool is_extended_binary(sat::ext_justification_idx idx, literal_vector& r) override;
         bool is_external(bool_var v) override;
         void get_antecedents(literal l, sat::ext_justification_idx idx, literal_vector & r, bool probing) override;
+        euf::enode_pair get_justification_eq(size_t j) override;
         void asserted(literal l) override;
         sat::check_result check() override;
         void push_core() override;

src/sat/smt/euf_proof.cpp

@@ -43,6 +43,13 @@ namespace euf {
         m_proof_initialized = true;        
     }
 
+    enode_pair solver::get_justification_eq(size_t j) {
+        auto* ext = sat::constraint_base::to_extension(j);
+        SASSERT(ext != this);
+        auto s = fid2solver(ext->get_id());
+        return s->get_justification_eq(j);
+    }
+
     /**
     * Log justifications.
     * is_euf - true if l is justified by congruence closure. In this case create a congruence closure proof.
@@ -63,7 +70,8 @@ namespace euf {
                 if (is_literal(e))
                     m_hint_lits.push_back(get_literal(e));
                 else {
-                    auto [x, y] = th_explain::from_index(get_justification(e)).eq_consequent();
+                    SASSERT(is_justification(e));
+                    auto [x, y] = get_justification_eq(get_justification(e));
                     eqs.push_back(m.mk_eq(x->get_expr(), y->get_expr()));
                     set_tmp_bool_var(nv, eqs.back());
                     m_hint_lits.push_back(literal(nv, false));

src/sat/smt/euf_solver.cpp

@@ -278,9 +278,9 @@ namespace euf {
                 r.push_back(get_literal(e));            
             else {
                 multiple_theories = true;
-                size_t idx = get_justification(e);
+                size_t idx = get_justification(e);                
                 auto* ext = sat::constraint_base::to_extension(idx);
-                SASSERT(ext != this);
+                SASSERT(ext != this);             
                 sat::literal lit = sat::null_literal;
                 ext->get_antecedents(lit, idx, r, probing);
             }
@@ -307,11 +307,11 @@ namespace euf {
     void solver::get_eq_antecedents(enode* a, enode* b, literal_vector& r) {
         m_egraph.begin_explain();
         m_explain.reset();
-	m_egraph.explain_eq<size_t>(m_explain, nullptr, a, b);
-	for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
-	    size_t* e = m_explain[qhead];
-	    if (is_literal(e)) 
-	        r.push_back(get_literal(e));            
+	    m_egraph.explain_eq<size_t>(m_explain, nullptr, a, b);
+	    for (unsigned qhead = 0; qhead < m_explain.size(); ++qhead) {
+	        size_t* e = m_explain[qhead];
+	        if (is_literal(e)) 
+	            r.push_back(get_literal(e));            
             else {
                 size_t idx = get_justification(e);
                 auto* ext = sat::constraint_base::to_extension(idx);

src/sat/smt/euf_solver.h

@@ -231,6 +231,7 @@ namespace euf {
         void log_antecedents(literal l, literal_vector const& r, th_proof_hint* hint);
         void log_justification(literal l, th_explain const& jst);
         void log_justifications(literal l, unsigned explain_size, bool is_euf);
+        enode_pair get_justification_eq(size_t j);
         void log_rup(literal l, literal_vector const& r);
 
 

src/sat/smt/sat_th.cpp

@@ -51,6 +51,10 @@ namespace euf {
         return true;
     }
 
+    enode_pair th_solver::get_justification_eq(size_t j) {
+        return th_explain::from_index(j).eq_consequent();
+    }
+
     th_euf_solver::th_euf_solver(euf::solver& ctx, symbol const& name, euf::theory_id id):
         th_solver(ctx.get_manager(), name, id),
         ctx(ctx)

src/sat/smt/sat_th.h

@@ -137,6 +137,8 @@ namespace euf {
 
         sat::status status() const { return sat::status::th(false, get_id()); }
 
+        virtual euf::enode_pair get_justification_eq(size_t j);
+
         /**
         * Local search interface
         */