diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml index 06f22621888faa482c6ca07a911865611f9782c8..046503fd821def58ece8ecbe496fee4fbb494a84 100644 --- a/src_colibri2/theories/LRA/fourier.ml +++ b/src_colibri2/theories/LRA/fourier.ml @@ -259,7 +259,8 @@ let converter d (f:Ground.t) = IArray.iter ~f:attach args; Egraph.attach_value d (Ground.node f) Boolean.dom Daemon.key (); Datastructure.Push.push comparisons d f; - Egraph.register_delayed_event d Daemon.key () + Egraph.register_delayed_event d Daemon.key (); + Egraph.register_decision d (Boolean.chobool (Ground.node f)) | _ -> () let init env = diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml index ad5c4d0bbe39f6bd8d38e7e1dd92d04e9b0a48a1..aff3d50e49c0010d5002d7cbeb0477382cf96bf5 100644 --- a/src_colibri2/theories/bool/boolean.ml +++ b/src_colibri2/theories/bool/boolean.ml @@ -323,9 +323,6 @@ let converter d (f:Ground.t) = | { app = {builtin = Expr.False}; tyargs = []; args; _ } -> assert ( IArray.is_empty args); reg _false - | { ty; _ } - when Ground.Ty.equal ty Ground.Ty.bool -> - Egraph.register_decision d (chobool res) | _ -> ()