mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 16:45:31 +00:00
parent
9f386306ef
commit
1155db383e
2 changed files with 2 additions and 0 deletions
|
@ -164,6 +164,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
void context::pop(unsigned n) {
|
||||
n = std::min(n, m_scoped_state.num_scopes());
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
m_scoped_state.pop();
|
||||
}
|
||||
|
|
|
@ -133,6 +133,7 @@ namespace opt {
|
|||
m_hard(m),
|
||||
m_asms(m)
|
||||
{}
|
||||
unsigned num_scopes() const { return m_hard_lim.size(); }
|
||||
void push();
|
||||
void pop();
|
||||
void add(expr* hard);
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue