michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/expr_lt): fix bug when using hash codes

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-14 13:18:33 -08:00
parent b0322787ff
commit 8e56726116
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/expr_lt.cpp
View file

@ -12,7 +12,10 @@ bool is_lt(expr const & a, expr const & b, bool use_hash) {
if (!a && b) return true; // the null expression is the smallest one
if (a && !b) return false;
if (a.kind() != b.kind()) return a.kind() < b.kind();
if (use_hash && a.hash() < b.hash()) return true;
if (use_hash) {
if (a.hash() < b.hash()) return true;
if (a.hash() > b.hash()) return false;
}
if (a == b) return false;
if (is_var(a)) return var_idx(a) < var_idx(b);
switch (a.kind()) {