From 5d07d456dcdb67cf6337af3fa146198e2fc8ce94 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 26 Jun 2023 00:40:31 -0400
Subject: [PATCH] fix sign error

---
 src/th-lra/sidekick_th_lra.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/th-lra/sidekick_th_lra.ml b/src/th-lra/sidekick_th_lra.ml
index 607753bb..94d54205 100644
--- a/src/th-lra/sidekick_th_lra.ml
+++ b/src/th-lra/sidekick_th_lra.ml
@@ -411,7 +411,7 @@ module Make (A : ARG) = (* : S with module A = A *) struct
         else (
           let le_comb_minus_t =
             var_encoding_comb ~pre:"diff_def" self
-              LE_.Comb.(le_comb - monomial1 box_t)
+              LE_.Comb.(monomial1 box_t - le_comb)
           in
           SimpSolver.add_constraint self.simplex
             (SimpSolver.Constraint.geq le_comb_minus_t le_const) Tag.By_def