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

harness more pop uses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-31 08:42:19 -07:00
parent 42d30e3edd
commit 98d42421bc
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/solver/tactic2solver.cpp
View file

@ -125,6 +125,7 @@ void tactic2solver::push_core() {
}
void tactic2solver::pop_core(unsigned n) {
n = std::min(m_scopes.size(), n);
unsigned new_lvl = m_scopes.size() - n;
unsigned old_sz = m_scopes[new_lvl];
m_assertions.shrink(old_sz);
@ -142,9 +143,8 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
m_tactic->updt_params(get_params()); // parameters are allowed to overwrite logic.
goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
unsigned sz = m_assertions.size();
for (unsigned i = 0; i < sz; i++) {
g->assert_expr(m_assertions.get(i));
for (expr* e : m_assertions) {
g->assert_expr(e);
}
for (unsigned i = 0; i < num_assumptions; i++) {
proof_ref pr(m.mk_asserted(assumptions[i]), m);