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

theory_fpa refactoring

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-31 16:22:48 +01:00
parent 302c491535
commit 47e75827ee
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_fpa.cpp
View file

@ -132,13 +132,13 @@ namespace smt {
m_converter.reset(); m_converter.reset();
m_rw.reset(); m_rw.reset();
m_th_rw.reset(); m_th_rw.reset();
m_is_initialized = false;
} }
SASSERT(m_trail_stack.get_num_scopes() == 0); SASSERT(m_trail_stack.get_num_scopes() == 0);
SASSERT(m_conversions.empty()); SASSERT(m_conversions.empty());
SASSERT(m_is_added_to_model.empty()); SASSERT(m_is_added_to_model.empty());
} }
void theory_fpa::init(context * ctx) { void theory_fpa::init(context * ctx) {
smt::theory::init(ctx); smt::theory::init(ctx);
m_is_initialized = true; m_is_initialized = true;
@ -710,10 +710,11 @@ namespace smt {
pop_scope_eh(m_trail_stack.get_num_scopes()); pop_scope_eh(m_trail_stack.get_num_scopes());
m_converter.reset(); m_converter.reset();
m_rw.reset(); m_rw.reset();
m_th_rw.reset(); m_th_rw.reset();
m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
if (m_factory) dealloc(m_factory); m_factory = 0;
ast_manager & m = get_manager(); ast_manager & m = get_manager();
dec_ref_map_key_values(m, m_conversions); dec_ref_map_key_values(m, m_conversions);
dec_ref_collection_values(m, m_is_added_to_model); dec_ref_collection_values(m, m_is_added_to_model);
theory::reset_eh(); theory::reset_eh();
} }