Basile Clément

Following dev meeting, here is an example of a file where this code is not dead: ```smt-lib2 (set-logic ALL) (declare-const a (Array Bool Bool)) (declare-const x Int) (declare-const y Int)...

I expected this to have little to no impact but there seems to be some regressions on the internal dataset. I don't think we need it for 2.6.0 as the...

Sure — I think it will be mostly identical once it is posted again, but I want to make sure I understand the regressions better. If needed we will keep...

This should have been fixed in #936 but seems we re-introduced the issue. I am not sure why you can't add labels; I think this needs you to have the...

Turns out the fix in #936 only applies if the step limit is reached while processing an assertion, not while processing `(check-sat)`. > Moreover: we want the prover to continue,...

I meant that the year should ideally depend on the file. If we can't do that, keeping the start of the project date (2013) everywhere is better.

I don't really see the point of this format: the main point here is to not claim copyright before the code was actually written. So ideally we would have `XXXX...

I think this is correct wrt the files changed. I understood we chose the option of keeping "2013 - 2024" everywhere, but dropping the years is fine by me should...

Note: we should use step bounds for reproducible-resource-limit (but we don't support per-goal step bounds at the moment). As per the SMT-LIB specification it must be guaranteed that running the...

> I think that a decent fix consists in applying a substitution on representative terms before generating model terms. This substitution replaces fresh leaves by abstract ones and we have...