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

fixed bug in solver_na2as

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-02 11:36:59 -07:00
parent 33c165490c
commit e1eb3ee8ee
2 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/ni_solver.cpp
View file

@ -77,7 +77,7 @@ public:
} }
void init_solver() { void init_solver() {
reset(); reset_core();
#pragma omp critical (ni_solver) #pragma omp critical (ni_solver)
{ {
m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params()); m_context = alloc(smt::kernel, m_cmd_ctx.m(), m_cmd_ctx.params());

13
src/solver/solver_na2as.cpp
View file

@ -26,15 +26,15 @@ solver_na2as::solver_na2as() {
} }
solver_na2as::~solver_na2as() { solver_na2as::~solver_na2as() {
if (m_manager) restore_assumptions(0);
restore_assumptions(0);
} }
void solver_na2as::assert_expr(expr * t, expr * a) { void solver_na2as::assert_expr(expr * t, expr * a) {
SASSERT(m_manager != 0); SASSERT(m_manager != 0);
expr * new_t = m_manager->mk_implies(a, t);
m_manager->inc_ref(a); m_manager->inc_ref(a);
m_assumptions.push_back(a); m_assumptions.push_back(a);
expr_ref new_t(*m_manager);
new_t = m_manager->mk_implies(a, t);
assert_expr(new_t); assert_expr(new_t);
} }
@ -62,7 +62,7 @@ struct append_assumptions {
lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) { lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptions) {
append_assumptions app(m_assumptions, num_assumptions, assumptions); append_assumptions app(m_assumptions, num_assumptions, assumptions);
return check_sat_core(num_assumptions, assumptions); return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr());
} }
void solver_na2as::push() { void solver_na2as::push() {
@ -80,7 +80,7 @@ void solver_na2as::pop(unsigned n) {
} }
void solver_na2as::restore_assumptions(unsigned old_sz) { void solver_na2as::restore_assumptions(unsigned old_sz) {
SASSERT(m_manager); SASSERT(old_sz == 0 || m_manager != 0);
for (unsigned i = old_sz; i < m_assumptions.size(); i++) { for (unsigned i = old_sz; i < m_assumptions.size(); i++) {
m_manager->dec_ref(m_assumptions[i]); m_manager->dec_ref(m_assumptions[i]);
} }
@ -93,6 +93,5 @@ unsigned solver_na2as::get_scope_level() const {
void solver_na2as::reset() { void solver_na2as::reset() {
reset_core(); reset_core();
if (m_manager) restore_assumptions(0);
restore_assumptions(0);
} }