mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

possible fix for #7255

Browse source
This commit is contained in:
hgvk94 2024-08-03 09:31:21 -04:00
parent 51fcb10b2f
commit be0707dc91
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_array_base.cpp
View file

@ -562,7 +562,7 @@ namespace smt {
theory_var v2 = *it2;
enode * n2 = get_enode(v2);
sort * s2 = n2->get_expr()->get_sort();
if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
if (s1 == s2 && !ctx.is_diseq(n1, n2) && !m.are_distinct(n1->get_expr(), n2->get_expr())) {
app * eq = mk_eq_atom(n1->get_expr(), n2->get_expr());
if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
result++;