mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-07 15:55:46 +00:00
Code Activity

revert to logging conflict to get EUF trim to work

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-25 09:45:35 -07:00
parent 6c8b8609ee
commit 68a437e615
6 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/cmd_context/extra_cmds/proof_cmds.cpp
View file

@ -350,9 +350,9 @@ public:
void updt_params(params_ref const& p) override {
solver_params sp(p);
m_check = sp.proof_check();
m_save = sp.proof_save();
m_trim = sp.proof_trim();
m_check = sp.proof_check() && !m_trim && !m_save && !m_on_clause_eh;
if (m_trim)
trim().updt_params(p);
}
@ -360,6 +360,8 @@ public:
void register_on_clause(void* ctx, user_propagator::on_clause_eh_t& on_clause_eh) override {
m_on_clause_ctx = ctx;
m_on_clause_eh = on_clause_eh;
if (m_on_clause_eh)
m_check = false;
}
};