mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix reset order for #4533
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
1204671595
commit
274323b818
|
@ -917,20 +917,23 @@ def is_CXX_clangpp():
|
|||
return is_clang_in_gpp_form(CXX)
|
||||
return is_compiler(CXX, 'clang++')
|
||||
|
||||
def get_files_with_ext(path, ext):
|
||||
return filter(lambda f: f.endswith(ext), os.listdir(path))
|
||||
|
||||
def get_cpp_files(path):
|
||||
return filter(lambda f: f.endswith('.cpp'), os.listdir(path))
|
||||
return get_files_with_ext(path,'.cpp')
|
||||
|
||||
def get_c_files(path):
|
||||
return filter(lambda f: f.endswith('.c'), os.listdir(path))
|
||||
return get_files_with_ext(path,'.c')
|
||||
|
||||
def get_cs_files(path):
|
||||
return filter(lambda f: f.endswith('.cs'), os.listdir(path))
|
||||
return get_files_with_ext(path,'.cs')
|
||||
|
||||
def get_java_files(path):
|
||||
return filter(lambda f: f.endswith('.java'), os.listdir(path))
|
||||
return get_files_with_ext(path,'.java')
|
||||
|
||||
def get_ml_files(path):
|
||||
return filter(lambda f: f.endswith('.ml'), os.listdir(path))
|
||||
return get_files_with_ext(path,'.ml')
|
||||
|
||||
def find_all_deps(name, deps):
|
||||
new_deps = []
|
||||
|
@ -2273,6 +2276,10 @@ def add_lib(name, deps=[], path=None, includes2install=[]):
|
|||
c = LibComponent(name, path, deps, includes2install)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_clib(name, deps=[], path=None, includes2install=[]):
|
||||
c = CLibComponent(name, path, deps, includes2install)
|
||||
reg_component(name, c)
|
||||
|
||||
def add_hlib(name, path=None, includes2install=[]):
|
||||
c = HLibComponent(name, path, includes2install)
|
||||
reg_component(name, c)
|
||||
|
|
|
@ -2677,8 +2677,8 @@ namespace smt2 {
|
|||
SASSERT(curr_id() == m_reset);
|
||||
next();
|
||||
check_rparen("invalid reset command, ')' expected");
|
||||
reset();
|
||||
m_ctx.reset();
|
||||
reset();
|
||||
m_ctx.print_success();
|
||||
next();
|
||||
}
|
||||
|
@ -3077,17 +3077,18 @@ namespace smt2 {
|
|||
m_pattern_stack = nullptr;
|
||||
m_nopattern_stack = nullptr;
|
||||
m_sexpr_stack = nullptr;
|
||||
m_bv_util = nullptr;
|
||||
m_arith_util = nullptr;
|
||||
m_seq_util = nullptr;
|
||||
m_pattern_validator = nullptr;
|
||||
m_var_shifter = nullptr;
|
||||
m_symbol_stack .reset();
|
||||
m_param_stack .reset();
|
||||
m_env .reset();
|
||||
m_sort_id2param_idx .reset();
|
||||
m_dt_name2idx .reset();
|
||||
|
||||
m_bv_util = nullptr;
|
||||
m_arith_util = nullptr;
|
||||
m_seq_util = nullptr;
|
||||
m_pattern_validator = nullptr;
|
||||
m_var_shifter = nullptr;
|
||||
|
||||
}
|
||||
|
||||
sexpr_ref parse_sexpr_ref() {
|
||||
|
|
Loading…
Reference in a new issue