Basile Clément
Basile Clément
I believe equalities found here ultimately end up in [Ccx.make_unique](https://github.com/OCamlPro/alt-ergo/blob/fb0293a28be8e29e6f9df6aba8ac23933857c62b/src/lib/reasoners/ccx.ml#L448) which does deduplicate. I think usually we won't find too much duplicates here (at most the number of constraints anyways)...
Alt-ergo uses a weak hash table to store all the expressions that are created for hash consing. Unfortunately, this means that the behavior of alt-ergo depends on the behavior of...
As observed in #1004, there are issues with the BV theory where once we have split enough to determine the exact value of a bit-vector, we find a contradiction. But...
One step towards #919 (this issue is for using opam with Cygwin again, not native support)
Need to understand: - How the implementation actually relates to what is described in the paper, - What are the assumptions made about the orderings used in different places of...
It looks like some of the recent changes (I'd guess either #829 or #861 is the source) have broken timeout support badly. The core of the issue is that, since...
Would be good/useful to have one. https://ocaml.org/docs/guidelines might be a starting point. Related but not limited to #634 (while #634 can take care of the low-level details, there are still...
I believe both `Satml_types` and `Satml` modules actually sort of need to know its internals currently, so nothing major as far as I know. Making it an abstract type is...
Since we support polymorphic input in the SMT-LIB format, we should have at least a few minimal tests for that feature.