Bug in prenex handling of Or.

[AbdallahS]

See line

touist/src/lib/qbf.ml

Line 64 in 1bf1b52

| Or (f,Forall (x,g)) | Or (Forall (x,g),f) -> Forall (to_prenex x,And (to_prenex_rn x f,to_prenex_new x g)) (* 3,6 *)

. The And on the right-hand side needs to be Or. I'll fix it at some point, but it'd be nice to have some unit tests for the prenex transformation, for instance one that would detect this specific bug.

[AbdallahS]

There is also a type in

touist/src/lib/qbf.ml

Line 62 in 1bf1b52

| Not Forall (x,f) -> Forall (to_prenex x,Not (to_prenex_new x f)) (* 1 *)

on the right-hand side, the forall should be an exists.