From df2eb771ef160aaa06719cb60e8ec41e86bfd30a Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 15 May 2018 09:55:04 -0700 Subject: [PATCH] Fix in spacer_itp_solver: use pr.get() instead of get_proof() --- src/muz/spacer/spacer_itp_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/spacer/spacer_itp_solver.cpp b/src/muz/spacer/spacer_itp_solver.cpp index 07c5f5871..f91cc6bb3 100644 --- a/src/muz/spacer/spacer_itp_solver.cpp +++ b/src/muz/spacer/spacer_itp_solver.cpp @@ -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);