From fb5a40a6fd801249e42add802c892bae878390b3 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 13 May 2024 15:14:49 +0200 Subject: [PATCH] fix sle --- src/sat/smt/polysat/constraints.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/sat/smt/polysat/constraints.h b/src/sat/smt/polysat/constraints.h index 23e801ce1..e6bdbe183 100644 --- a/src/sat/smt/polysat/constraints.h +++ b/src/sat/smt/polysat/constraints.h @@ -153,14 +153,13 @@ namespace polysat { signed_constraint slt(int p, pdd const& q) { return slt(rational(p), q); } signed_constraint slt(unsigned p, pdd const& q) { return slt(rational(p), q); } - signed_constraint sgt(pdd const& p, pdd const& q) { return slt(q, p); } signed_constraint sgt(pdd const& p, int q) { return slt(q, p); } signed_constraint sgt(pdd const& p, unsigned q) { return slt(q, p); } signed_constraint sgt(int p, pdd const& q) { return slt(q, p); } signed_constraint sgt(unsigned p, pdd const& q) { return slt(q, p); } - signed_constraint sge(pdd const& p, pdd const& q) { return ~slt(q, p); } + signed_constraint sge(pdd const& p, pdd const& q) { return sle(q, p); } signed_constraint sge(pdd const& p, int q) { return sge(p, p.manager().mk_val(q)); } signed_constraint umul_ovfl(pdd const& p, rational const& q) { return umul_ovfl(p, p.manager().mk_val(q)); }