From 791290118b4fef916a0cf49f50c019dfeedc116e Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 18 Mar 2021 12:26:14 -0400 Subject: [PATCH] fix(form): make eval rule more precise --- src/smtlib/Form.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml index 76faabc4..d9204332 100644 --- a/src/smtlib/Form.ml +++ b/src/smtlib/Form.ml @@ -53,7 +53,7 @@ module Funs = struct | B_or a when Iter.for_all Value.is_false a -> Value.false_ | B_imply (_, V_bool true) -> Value.true_ | B_imply (a,_) when Iter.exists Value.is_false a -> Value.true_ - | B_imply (a,b) when Iter.for_all Value.is_bool a && Value.is_bool b -> Value.false_ + | B_imply (a,b) when Iter.for_all Value.is_true a && Value.is_false b -> Value.false_ | B_ite(a,b,c) -> if Value.is_true a then b else if Value.is_false a then c