From ffc45b0db6b873ceb987b581612df50e38975f81 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 18 Mar 2021 18:20:39 -0400 Subject: [PATCH] fix: do not preemptively simplify `imply` --- src/th-bool-static/Sidekick_th_bool_static.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 96efc8d0..a177b2da 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -105,13 +105,9 @@ module Make(A : ARG) : S with module A = A = struct else if Iter.for_all is_false a then Some (T.bool tst false) else None | B_imply (args, u) -> - (* turn into a disjunction *) - let u = - let args = - args |> Iter.map (not_ tst) |> IArray.of_iter in - or_a tst @@ IArray.append args (IArray.singleton u) - in - Some u + if Iter.exists is_false args then Some (T.bool tst true) + else if is_true u then Some (T.bool tst true) + else None | B_ite (a,b,c) -> (* directly simplify [a] so that maybe we never will simplify one of the branches *)