simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 05:28:34 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(form): make eval rule more precise

Browse source
This commit is contained in:
Simon Cruanes 2021-03-18 12:26:14 -04:00
parent 07ca5546f5
commit 791290118b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smtlib/Form.ml
View file

@ -53,7 +53,7 @@ module Funs = struct
| B_or a when Iter.for_all Value.is_false a -> Value.false_ | B_or a when Iter.for_all Value.is_false a -> Value.false_
| B_imply (_, V_bool true) -> Value.true_ | B_imply (_, V_bool true) -> Value.true_
| B_imply (a,_) when Iter.exists Value.is_false a -> 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) -> | B_ite(a,b,c) ->
if Value.is_true a then b if Value.is_true a then b
else if Value.is_false a then c else if Value.is_false a then c