mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5300

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-28 14:16:43 -07:00
parent f42d4a58e3
commit c5d4ff9b6f
2 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/cmd_context/cmd_context.cpp
View file

@ -611,6 +611,7 @@ void cmd_context::set_produce_models(bool f) {
} }
void cmd_context::set_produce_unsat_cores(bool f) { void cmd_context::set_produce_unsat_cores(bool f) {
std::cout << "uc\n";
// can only be set before initialization // can only be set before initialization
SASSERT(!has_manager()); SASSERT(!has_manager());
m_params.m_unsat_core |= f; m_params.m_unsat_core |= f;

3
src/cmd_context/cmd_context_to_goal.cpp
View file

@ -25,13 +25,14 @@ Notes:
void assert_exprs_from(cmd_context const & ctx, goal & t) { void assert_exprs_from(cmd_context const & ctx, goal & t) {
if (ctx.produce_proofs() && ctx.produce_unsat_cores()) if (ctx.produce_proofs() && ctx.produce_unsat_cores())
throw cmd_exception("Frontend does not support simultaneous generation of proofs and 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(); ast_manager & m = t.m();
bool proofs_enabled = t.proofs_enabled(); bool proofs_enabled = t.proofs_enabled();
if (ctx.produce_unsat_cores()) { if (ctx.produce_unsat_cores()) {
ptr_vector<expr>::const_iterator it = ctx.assertions().begin(); ptr_vector<expr>::const_iterator it = ctx.assertions().begin();
ptr_vector<expr>::const_iterator end = ctx.assertions().end(); ptr_vector<expr>::const_iterator end = ctx.assertions().end();
ptr_vector<expr>::const_iterator it2 = ctx.assertion_names().begin(); ptr_vector<expr>::const_iterator it2 = ctx.assertion_names().begin();
SASSERT(ctx.assertions().size() == ctx.assertion_names().size());
for (; it != end; ++it, ++it2) { for (; it != end; ++it, ++it2) {
t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, m.mk_leaf(*it2)); t.assert_expr(*it, proofs_enabled ? m.mk_asserted(*it) : nullptr, m.mk_leaf(*it2));
} }