diff options
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index 2c83b32..262bccb 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -69,13 +69,17 @@ and conslist_bool_expr = let rec conslist_of_f = function | BNot e -> conslist_of_f (eliminate_not_negate e) | BRel (op, a, b) -> - let cons = match op with - | AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ - | AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE - | AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT - | AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE - | AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT - | AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE + let x, y, op = match op with + | AST_EQ -> a, b, CONS_EQ + | AST_NE -> a, b, CONS_NE + | AST_GT -> a, b, CONS_GT + | AST_GE -> a, b, CONS_GE + | AST_LT -> b, a, CONS_GT + | AST_LE -> b, a, CONS_GE + in + let cons = if y = NIntConst 0 + then (x, op) + else (NBinary(AST_MINUS, x, y), op) in [cons], CLTrue | BConst x -> [], if x then CLTrue else CLFalse |