Pierre Villemot
Pierre Villemot
> I think that this is because we never call `Uf.make` on unused symbols, and we probably don't want to do that so as to avoid overloading the data structure....
Exactly! We have to clean up the way we use ID in the UF before fixing this issue.
Besides, I hope `Dolmen` works on Windows. I think @Gbury did the job to make it works ;)
The issue has been solved by the PR https://github.com/Gbury/dolmen/pull/175 on Dolmen but the fix hasn't been released yet.
A hot fix have been merged on the branch `v2.5.x` for the release `v2.5.2`, see #890.
After some offline discussions, it seems that solving the issue is not a priority for the next release as we don't expect to see valuable performance improvements because of the...
Both bugs should be solve by pushing case splits in SAT solvers. The current implementation doesn't restore completely the environment of the module `Theory` after a pop statement.
@bclement-ocp 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...
This bug have been fixed in `Dune` indeed.
I totally agree that we should get rid of it as soon as possible. But we should be sure the actually parser in Dolmen behaves closely like the legacy one....