diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml index 422a926cc9a5ce6958553ed25225c1f1715b6a68..bd52c9dc7bda66cd4a7d37e6c6e474fe04db7095 100644 --- a/src/lib/CoAlgFormula.ml +++ b/src/lib/CoAlgFormula.ml @@ -153,7 +153,7 @@ let rec convert_post func formula = (* run over all subformulas in post order *) (* replace parts of the formula *) let formula = (match formula with (* 0-ary constructors *) - | TRUE | FALSE | AP _ -> formula + | TRUE | FALSE | AP _ | VAR _ -> formula | CONST _ | CONSTN _ -> formula (* unary *) @@ -178,7 +178,15 @@ let rec convert_post func formula = (* run over all subformulas in post order *) | NORM(a, b) -> NORM(c a, c b) | NORMN(a, b) -> NORMN(c a, c b) | CHC (a,b) -> CHC (c a, c b) - | FUS (s,a) -> FUS (s, c a)) in + | FUS (s,a) -> FUS (s, c a) + | MU (n, f1) -> MU (n, c f1) + | NU (n, f1) -> NU (n, c f1) + | AF f1 -> AF (c f1) + | EF f1 -> EF (c f1) + | AG f1 -> AG (c f1) + | EG f1 -> EG (c f1) + | AU (f1, f2) -> AU (c f1, c f2) + | EU (f1, f2) -> AU (c f1, c f2))in func formula let convertToK formula = (* tries to convert a formula to a pure K formula *)