mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

proposed fix to compare

Browse source
This commit is contained in:
Arie Gurfinkel 2016-03-23 19:20:27 -04:00
parent ee125b4fe3
commit 4e7b6b6586
1 changed files with 4 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/qe/qe_arrays.cpp
View file

@ -397,16 +397,15 @@ namespace qe {
} }
lbool compare(expr* val1, expr* val2) { lbool compare(expr* val1, expr* val2) {
if (val1 == val2) { if (m.are_equal (val1, val2)) return l_true;
return l_true; if (m.are_distinct (val1, val2)) return l_false;
}
if (is_uninterp(val1) || if (is_uninterp(val1) ||
is_uninterp(val2)) { is_uninterp(val2)) {
// TBD chase definition of nested array. // TBD chase definition of nested array.
return l_undef; return l_undef;
} }
// AG: Shouldn't this be l_false return l_undef;
return l_true;
} }
}; };