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

fix(kernel/level): add (trivial) case for is_geq predicate: l >= 0 for any l

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 18:13:50 -07:00
parent 045fa911d1
commit f816487f4b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/level.cpp
View file

@ -665,7 +665,7 @@ bool is_equivalent(level const & lhs, level const & rhs) {
}
bool is_geq_core(level l1, level l2) {
if (l1 == l2)
if (l1 == l2 || is_zero(l2))
return true;
if (is_max(l2))
return is_geq(l1, max_lhs(l2)) && is_geq(l1, max_rhs(l2));