mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

add warning for scearios of #876

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-25 18:29:30 -08:00
parent 6e6c5935d7
commit 7386e2f3e9
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_seq.cpp
View file

@ -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) {