Re-enable support for single-argument conjunctions and disjunctions in some form?

[blishko]

Recently (c537c75), carcara started enforcing strict SMT-LIB semantics and disallowed single-argument conjunctions and disjunctions.

We are checking CHC benchmarks using carcara and this became a problem, because CHC-COMP benchmarks are more permissive, and often contain single-argument conjunctions or disjunctions.
Would it be possible to re-enable support for such terms, possibly under some flag?

One possibility would be to enforce proper SMT-LIB semantics only in Carcara's strict checking mode.
Another would be to add a special option to support such exceptional terms (similar to --allow-int-real-subtyping)?

It would allow us to use original version of carcara and not a custom patched version.

[bpandreotti]

That is a reasonable request, and 71c1edc resolves this. We opted to allow these unary operations by default, and to reject them only if the --strict flag is passed. Maybe in the future it might make sense to split that flag into --strict-parsing/--strict-checking, but for now this works.