mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
Bugfix for inc_sat_solver
This commit is contained in:
parent
68416bf6bc
commit
bf40bb8005
|
@ -182,7 +182,7 @@ public:
|
|||
m_map.push();
|
||||
}
|
||||
virtual void pop(unsigned n) {
|
||||
if (n < m_num_scopes) { // allow inc_sat_solver to
|
||||
if (n > m_num_scopes) { // allow inc_sat_solver to
|
||||
n = m_num_scopes; // take over for another solver.
|
||||
}
|
||||
m_bb_rewriter.pop(n);
|
||||
|
|
Loading…
Reference in a new issue