From c5d4ff9b6ffc7d8f79ef36b840ddc65aa0a837f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 May 2021 14:16:43 -0700 Subject: [PATCH] fix #5300 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 + src/cmd_context/cmd_context_to_goal.cpp | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index fd8eeb3f1..315c26d95 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -611,6 +611,7 @@ void cmd_context::set_produce_models(bool f) { } void cmd_context::set_produce_unsat_cores(bool f) { + std::cout << "uc\n"; // can only be set before initialization SASSERT(!has_manager()); m_params.m_unsat_core |= f; diff --git a/src/cmd_context/cmd_context_to_goal.cpp b/src/cmd_context/cmd_context_to_goal.cpp index de19805f2..0b1644171 100644 --- a/src/cmd_context/cmd_context_to_goal.cpp +++ b/src/cmd_context/cmd_context_to_goal.cpp @@ -25,13 +25,14 @@ Notes: void assert_exprs_from(cmd_context const & ctx, goal & t) { if (ctx.produce_proofs() && ctx.produce_unsat_cores()) throw cmd_exception("Frontend does not support simultaneous generation of proofs and unsat cores"); + if (ctx.produce_unsat_cores() && ctx.assertions().size() != ctx.assertion_names().size()) + throw cmd_exception("Unsat core tracking must be set before assertions are added"); ast_manager & m = t.m(); bool proofs_enabled = t.proofs_enabled(); if (ctx.produce_unsat_cores()) { ptr_vector::const_iterator it = ctx.assertions().begin(); ptr_vector::const_iterator end = ctx.assertions().end(); ptr_vector::const_iterator it2 = ctx.assertion_names().begin(); - SASSERT(ctx.assertions().size() == ctx.assertion_names().size()); for (; it != end; ++it, ++it2) { t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, m.mk_leaf(*it2)); }