From 337c07a44c6a143165fc6a8c3f3c1bd7781bf45d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 11 Apr 2020 09:15:32 -0400 Subject: [PATCH] Fix #3788 by converting assert into a throw --- src/muz/spacer/spacer_sat_answer.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp index 5438436e3..9e0a18703 100644 --- a/src/muz/spacer/spacer_sat_answer.cpp +++ b/src/muz/spacer/spacer_sat_answer.cpp @@ -66,7 +66,7 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { lbool res = m_solver->check_sat(0, nullptr); CTRACE("spacer_sat", res != l_true, tout << "solver at check:\n"; m_solver->display(tout) << "res: " << res << "\n";); - VERIFY(res == l_true); + if (res != l_true) throw default_exception("spacer: could not validate first proof step"); model_ref mdl; m_solver->get_model(mdl); mdl->compress(); @@ -133,10 +133,10 @@ void ground_sat_answer_op::mk_children(frame &fr, vector &todo) { m_solver->display(tout) << "\n";); lbool res = m_solver->check_sat(0, nullptr); - (void)res; CTRACE("spacer_sat", res != l_true, - tout << "Result: " << res << "\n";); - VERIFY(res == l_true); + m_solver->display(tout) << "\n" "Result: " << res << "\n";); + if(res != l_true) + throw default_exception("spacer: could not validate a proof step"); model_ref mdl; m_solver->get_model(mdl);