Datatype theory seems to be builtin and always present about dolmen HOT 4 CLOSED

I did that? I believe the idea is still to define it only when DT is present, https://github.com/CVC4/CVC4/blob/fd60da4a22f02f6f5b82cef3585240c1b33595e9/src/theory/logic_info.cpp#L446 . As for every thing in SMTLIB the idea is to know if a solver will be able to support the benchmark or not, so since not every solver support it, it is better to mark the problem that use the feature with DT. But some benchmark could be wrongly without it, if solver doesn't enforce that. (Do you tried CVC4 with --strict-mode?)

from dolmen.

Oh, I didn't know about --strict-mode, I'll try that.
On that note, dolmen now has a --strict=<bool> option, though the default is true (i.e. strictly respect the spec), and --strict=false can be used to have some more lenient typechecking.

from dolmen.

From what I can tell, datatypes is part of the core of the language, see e.g. page 84 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf :

Recall that algebraic datatypes are not defined in theories but directly at the level of the underlying SMT-LIB logic

So dolmen should probably allow datatypes regardless of the theory/logic that is set for a file.

from dolmen.

Ok, so after a few discussions, the current behavior of dolmen, i.e. to only accept datatypes definitions when DT is present in the logic, seems to be the right one, so let's close this one for now, ^^

from dolmen.