mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Fix in spacer_itp_solver: use pr.get() instead of get_proof()

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-15 09:55:04 -07:00
parent ab3a6702af
commit df2eb771ef
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/spacer/spacer_itp_solver.cpp
View file

@ -287,8 +287,8 @@ void itp_solver::get_itp_core (expr_ref_vector &core)
);
// construct proof object with contains partition information
iuc_proof iuc_pr(m, get_proof(), B);
iuc_proof iuc_pr(m, pr.get(), B);
// configure learner
unsat_core_learner learner(m, iuc_pr, m_print_farkas_stats, m_iuc_debug_proof);