mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 18:15:32 +00:00
Code Activity

clear tactic user propagate state on solver destructor

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-07 03:11:54 -08:00
parent fdc253afdd
commit 658a334ecf
4 changed files with 23 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/solver/tactic2solver.cpp
View file

@ -112,6 +112,11 @@ public:
return m_tactic->user_propagate_register(e);
}
void user_propagate_clear() override {
if (m_tactic)
m_tactic->user_propagate_clear();
}
expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override {
set_reason_unknown("cubing is not supported on tactics");
@ -148,6 +153,7 @@ tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p,
}
tactic2solver::~tactic2solver() {
user_propagate_clear();
}
void tactic2solver::updt_params(params_ref const & p) {