Basile Clément
Basile Clément
Well I tried with `last-4.14` but I get a bunch of errors due to unused variables and magic potions. Will ask the flambda team.
I have spent some more time implementing a better version of this, but hit another blocker. The crux of it is that Alt-Ergo has many copies of the union-find data...
> I am not sure the solution you suggested can works well. As I mentioned it, the objectives are registered in the theory environments. These environments are backtracked but all...
I have not experienced this in quite some time. I suggest we close as probably fixed in `dune` if it does not occur again in the next 3 months.
For reference: #432 is the PR that introduced the flattening
Blocked by #585 and #586
Yes, `--model-output` should be removed and we should be smtlib2-compliant if/where possible. smtlib2 has two output channels: the regular output channel and the diagnostic output channel, which defaults to `stdout`...
Note: I am seeing some crashes with these changes that I thought I had eliminated, marking the PR as draft until I figure it out.
Does the problem also happen with the Tableaux solver? I remember that it seemed to behave better wrt instantiation in some tests I made while looking at the differences a...
> Good catch! It works with the option `--sat-solver Tableaux`. Ha! That confirms an intuition I had that we should be looking precisely at the difference in the way the...