mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

fix #3389

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-18 10:36:34 -07:00
parent a45532da73
commit b590751e92
2 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_seq.cpp
View file

@ -302,6 +302,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_internalize_depth(0), m_internalize_depth(0),
m_ls(m), m_rs(m), m_ls(m), m_rs(m),
m_lhs(m), m_rhs(m), m_lhs(m), m_rhs(m),
m_has_seq(m_util.has_seq()),
m_res(m), m_res(m),
m_max_unfolding_depth(1), m_max_unfolding_depth(1),
m_max_unfolding_lit(null_literal), m_max_unfolding_lit(null_literal),
@ -344,7 +345,7 @@ struct scoped_enable_trace {
}; };
final_check_status theory_seq::final_check_eh() { final_check_status theory_seq::final_check_eh() {
if (!m_util.has_seq()) { if (!m_has_seq) {
return FC_DONE; return FC_DONE;
} }
m_new_propagation = false; m_new_propagation = false;
@ -3755,6 +3756,7 @@ bool theory_seq::internalize_atom(app* a, bool) {
} }
bool theory_seq::internalize_term(app* term) { bool theory_seq::internalize_term(app* term) {
m_has_seq = true;
context & ctx = get_context(); context & ctx = get_context();
if (ctx.e_internalized(term)) { if (ctx.e_internalized(term)) {
enode* e = ctx.get_enode(term); enode* e = ctx.get_enode(term);
@ -6444,7 +6446,7 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
} }
void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
if (m_util.has_seq()) { if (m_has_seq) {
TRACE("seq", tout << "add_theory_assumption\n";); TRACE("seq", tout << "add_theory_assumption\n";);
expr_ref dlimit(m); expr_ref dlimit(m);
dlimit = mk_max_unfolding_depth(); dlimit = mk_max_unfolding_depth();
@ -6456,7 +6458,7 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
bool theory_seq::should_research(expr_ref_vector & unsat_core) { bool theory_seq::should_research(expr_ref_vector & unsat_core) {
TRACE("seq", tout << unsat_core << " " << m_util.has_re() << "\n";); TRACE("seq", tout << unsat_core << " " << m_util.has_re() << "\n";);
if (!m_util.has_seq()) { if (!m_has_seq) {
return false; return false;
} }
for (auto & e : unsat_core) { for (auto & e : unsat_core) {

1
src/smt/theory_seq.h
View file

@ -406,6 +406,7 @@ namespace smt {
ptr_vector<expr> m_todo, m_concat; ptr_vector<expr> m_todo, m_concat;
unsigned m_internalize_depth; unsigned m_internalize_depth;
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs; expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
bool m_has_seq;
// maintain automata with regular expressions. // maintain automata with regular expressions.
scoped_ptr_vector<eautomaton> m_automata; scoped_ptr_vector<eautomaton> m_automata;