From 566348216fff4b119559d907df9b8e2e005fa023 Mon Sep 17 00:00:00 2001
From: stilscher <66023521+stilscher@users.noreply.github.com>
Date: Fri, 17 Nov 2023 16:14:36 +0100
Subject: [PATCH] improve values of parameters in abs call

---
 src/analyses/baseInvariant.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 72e00efbb1..73a41bcea1 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -726,6 +726,8 @@ struct
                             | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st
                             | `Lifted (Islessequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Le, xFloat, yFloat, (typeOf xFloat))) st
                             | `Lifted (Islessgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (LOr, (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))), (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))), (TInt (IBool, [])))) st
+                            | `Lifted (Abs xInt) ->
+                              inv_exp (Int (ID.of_bool ik tv)) (BinOp (LAnd, (BinOp (Le, xInt, Lval x, TInt (IInt,[]))), (BinOp (Le, (UnOp (Neg, Lval x, (typeOf xInt))), xInt, TInt (IInt,[]))), (TInt (IInt, [])))) st
                             | _ -> update_lval c x c' ID.pretty
                           end
                         | None -> update_lval c x c' ID.pretty