summaryrefslogtreecommitdiff
path: root/abstract/formula.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/formula.ml')
-rw-r--r--abstract/formula.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 01f6655..9c0ff71 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -51,7 +51,8 @@ type bool_expr =
| BNot of bool_expr
let f_and a b = match a, b with
- | BConst false, _ | _, BConst false -> BConst false
+ | BConst false, _ | _, BConst false
+ | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false
| BConst true, b -> b
| a, BConst true -> a
| a, b -> BAnd(a, b)