Guillaume Bury

Typing smtlib3 is going to be a non-trivial task indeed. I've already started to think about the changes that would be required to properly handle it. Currently the main points...

I'll try and post something on the SMTLIB google group soon to raise my concerns (primarily about overloading + polymorphism as an infinite family of overloaded functions, which makes resolving...

Dolmen now has support for higher-order typing, which is a first step towards supporting smtlibv3.

Another example: some problems may contain solver-reserved identifiers, particularly when they are created from the output of some solvers (see e.g. https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_BV/-/blob/master/20190429-UltimateAutomizerSvcomp2019/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i_6.smt2 ), it would be useful to be able...

It's fairly recent addition indeed: PR #193 made it so that it is an error to use symbols that start with an `@` or a `.`. Indeed, the smtlib specification...

In the meantime, and depending on how many problems in the smtlib use such solver-reserved identifiers, I'll consider changing the error into a warning, which would be fatal by default,...

I've tried the `-cclib -static` option, and it doesn't work because I don't have static versions of gmp and mpfr installed (additionally it seems to be quite a not-so-good idea...

To be clear, the point of escaping was precisely to not print unicode in languages that don't support it. Basically, the idea of escaping would be to map every unicode...

I already started some work on branch `printer`, where there is some skeleton you can start from.

This will be greatly benefit from the typed terms now that there is a type-checker. I'll upstream some code from archsat soon to cover this feature.