mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

breaking change. Enforce append semantics everywhere for parameter updates #5744

Browse source 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
This commit is contained in:
Nikolaj Bjorner 2021-12-30 19:11:14 -08:00
parent e8833f4dac
commit fc77345bec
53 changed files with 101 additions and 98 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_solver.cpp
View file

@ -124,7 +124,7 @@ namespace {
smt_params m_smt_params_save;
void push_params() override {
m_params_save = params_ref();
m_params_save.reset();
m_params_save.copy(solver::get_params());
m_smt_params_save = m_smt_params;
}

3
src/smt/tactic/smt_tactic_core.cpp
View file

@ -127,7 +127,8 @@ public:
scoped_init_ctx(smt_tactic & o, ast_manager & m):m_owner(o) {
m_params = o.fparams();
m_params_ref = o.params();
m_params_ref.reset();
m_params_ref.append(o.params());
smt::kernel * new_ctx = alloc(smt::kernel, m, m_params, m_params_ref);
TRACE("smt_tactic", tout << "logic: " << o.m_logic << "\n";);
new_ctx->set_logic(o.m_logic);

2
src/smt/tactic/unit_subsumption_tactic.cpp
View file

@ -50,7 +50,7 @@ struct unit_subsumption_tactic : public tactic {
}
void updt_params(params_ref const& p) override {
m_params = p;
m_params.append(p);
// m_context.updt_params(p); does not exist.
}