diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 27354eac2..941cd21d4 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -37,7 +37,7 @@ namespace xr { } void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, - sat::literal_vector & r, bool probing) { + sat::literal_vector & r, bool probing, sat::proof_hint*& ph) { } diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h index 3da30c580..0748e1e9b 100644 --- a/src/sat/smt/xor_solver.h +++ b/src/sat/smt/xor_solver.h @@ -30,7 +30,7 @@ namespace xr { void asserted(sat::literal l) override; bool unit_propagate() override; - void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override; + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing, sat::proof_hint*& ph) override; void pre_simplify() override; void simplify() override;