mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 20:38:43 +00:00
fixed solver_na2as
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
d545f187f8
commit
33c165490c
|
@ -26,7 +26,8 @@ solver_na2as::solver_na2as() {
|
|||
}
|
||||
|
||||
solver_na2as::~solver_na2as() {
|
||||
reset();
|
||||
if (m_manager)
|
||||
restore_assumptions(0);
|
||||
}
|
||||
|
||||
void solver_na2as::assert_expr(expr * t, expr * a) {
|
||||
|
@ -91,6 +92,7 @@ unsigned solver_na2as::get_scope_level() const {
|
|||
}
|
||||
|
||||
void solver_na2as::reset() {
|
||||
reset_core();
|
||||
if (m_manager)
|
||||
restore_assumptions(0);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue