From b05f192acc620f6b4ea6b95b4ea785720f700806 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 30 Sep 2020 10:10:35 +0200
Subject: [PATCH] [logic] improve expr_to_predicate on boolean-like expressions

---
 src/kernel_services/ast_queries/logic_utils.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 7fa1fe6dfc7..701d83e7e20 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -442,6 +442,12 @@ let get_float_unop op typ =
   | TFloat(fkind,_) , Neg  -> float_builtin "neg" fkind
   | _ -> None
 
+let is_boolean_exp e =
+  match e.enode with
+  | BinOp(op,_,_,_) -> is_boolean_binop op
+  | UnOp(LNot,_,_) -> true
+  | _ -> false
+
 let rec expr_to_term ?(coerce=false) e =
   let loc = e.eloc in
   let typ = Cil.typeOf e in
@@ -550,6 +556,10 @@ and expr_to_predicate e =
   | BinOp(Le, a, b, _) -> prel Rle a b
   | BinOp(Gt, a, b, _) -> prel Rgt a b
   | BinOp(Ge, a, b, _) -> prel Rge a b
+  | BinOp(Eq, a, b, _) when Cil.isZero b && is_boolean_exp a ->
+    pnot @@ expr_to_predicate a
+  | BinOp(Ne, a, b, _) when Cil.isZero b && is_boolean_exp a ->
+    expr_to_predicate a
   | BinOp(Eq, a, b, _) -> prel Req a b
   | BinOp(Ne, a, b, _) -> prel Rneq a b
   | BinOp(LAnd, a, b, _) ->
-- 
GitLab