mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix #7445

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-11-10 14:40:04 -08:00
parent abd16740ce
commit 4f060dd2b1
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/cmd_context/basic_cmds.cpp
View file

@ -467,7 +467,7 @@ class set_option_cmd : public set_get_option_cmd {
ctx.set_produce_unsat_cores(to_bool(value)); ctx.set_produce_unsat_cores(to_bool(value));
} }
else if (m_option == m_produce_unsat_assumptions) { else if (m_option == m_produce_unsat_assumptions) {
check_not_initialized(ctx, m_produce_unsat_assumptions); check_no_assertions(ctx, m_produce_unsat_assumptions);
ctx.set_produce_unsat_assumptions(to_bool(value)); ctx.set_produce_unsat_assumptions(to_bool(value));
} }
else if (m_option == m_produce_models) { else if (m_option == m_produce_models) {
@ -626,6 +626,9 @@ public:
else if (opt == m_produce_assignments) { else if (opt == m_produce_assignments) {
print_bool(ctx, ctx.produce_assignments()); print_bool(ctx, ctx.produce_assignments());
} }
else if (opt == m_produce_unsat_assumptions) {
print_bool(ctx, ctx.produce_unsat_assumptions());
}
else if (opt == m_global_decls || opt == m_global_declarations) { else if (opt == m_global_decls || opt == m_global_declarations) {
print_bool(ctx, ctx.global_decls()); print_bool(ctx, ctx.global_decls());
} }