diff --git a/src/sat/smt/polysat_egraph.cpp b/src/sat/smt/polysat_egraph.cpp index 5c14aa752..56246c97b 100644 --- a/src/sat/smt/polysat_egraph.cpp +++ b/src/sat/smt/polysat_egraph.cpp @@ -114,13 +114,13 @@ namespace polysat { m_bv_plugin->super_slices(b, consume_slice); } - void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function& consume_eq) { + void solver::explain_slice(pvar pv, pvar pw, unsigned offset, std::function const& consume_eq) { euf::theory_var v = m_pddvar2var[pv]; euf::theory_var w = m_pddvar2var[pw]; m_bv_plugin->explain_slice(var2enode(v), offset, var2enode(w), consume_eq); } - void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function& consume_eq) { + void solver::explain_fixed(pvar pv, fixed_slice const& slice, std::function const& consume_eq) { euf::theory_var v = m_pddvar2var[pv]; expr_ref val(bv.mk_numeral(slice.value, slice.length), m); euf::enode* b = ctx.get_egraph().find(val); diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h index 3f42381c6..c70a89989 100644 --- a/src/sat/smt/polysat_solver.h +++ b/src/sat/smt/polysat_solver.h @@ -111,8 +111,8 @@ namespace polysat { sat::check_result intblast(); - void explain_slice(pvar v, pvar w, unsigned offset, std::function& consume); - void explain_fixed(pvar v, fixed_slice const& s, std::function& consume_eq); + void explain_slice(pvar v, pvar w, unsigned offset, std::function const& consume); + void explain_fixed(pvar v, fixed_slice const& s, std::function const& consume_eq); // internalize bool visit(expr* e) override;