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

fix #3756

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 11:32:53 -07:00
parent 54d981e88f
commit 077f2248ca
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_str.cpp
View file

@ -7496,6 +7496,12 @@ namespace smt {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
// workaround for #3756:
// the map existing_toplevel_exprs is never cleared on backtracking.
// to ensure the expressions are valid we persist validity of the
// expression throughout the lifetime of theory_str
m_trail.push_back(ex);
sort * ex_sort = m.get_sort(ex); sort * ex_sort = m.get_sort(ex);
sort * str_sort = u.str.mk_string_sort(); sort * str_sort = u.str.mk_string_sort();
sort * bool_sort = m.mk_bool_sort(); sort * bool_sort = m.mk_bool_sort();
@ -7689,6 +7695,10 @@ namespace smt {
candidate_model.reset(); candidate_model.reset();
expr * e = get_context().bool_var2expr(v); expr * e = get_context().bool_var2expr(v);
TRACE("str", tout << "assert: v" << v << " " << mk_pp(e, get_manager()) << " is_true: " << is_true << std::endl;); TRACE("str", tout << "assert: v" << v << " " << mk_pp(e, get_manager()) << " is_true: " << is_true << std::endl;);
DEBUG_CODE(
for (auto * f : existing_toplevel_exprs) {
SASSERT(f->get_ref_count() > 0);
});
if (!existing_toplevel_exprs.contains(e)) { if (!existing_toplevel_exprs.contains(e)) {
existing_toplevel_exprs.insert(e); existing_toplevel_exprs.insert(e);
set_up_axioms(e); set_up_axioms(e);