From f816487f4bb1cd0f336851e993735a3b06a1b0c1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jun 2014 18:13:50 -0700 Subject: [PATCH] fix(kernel/level): add (trivial) case for is_geq predicate: l >= 0 for any l Signed-off-by: Leonardo de Moura --- src/kernel/level.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index e98e1b186..1420ff41f 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -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));