diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index cdea02c48..3e1436aa6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3819,6 +3819,15 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { solve_eqs(m_eqs.size()-1); enforce_length_coherence(n1, n2); } + else if (n1 != n2 && m_util.is_re(n1->get_owner())) { + warning_msg("equality between regular expressions is not yet supported"); + eautomaton* a1 = get_automaton(n1->get_owner()); + eautomaton* a2 = get_automaton(n2->get_owner()); + // eautomaton* b1 = mk_difference(*a1, *a2); + // eautomaton* b2 = mk_difference(*a2, *a1); + // eautomaton* c = mk_union(*b1, *b2); + // then some emptiness check. + } } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {