From 7386e2f3e942b025d8266323dc299055a7dd1efa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Jan 2017 18:29:30 -0800 Subject: [PATCH] add warning for scearios of #876 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) 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) {