alt-ergo
alt-ergo copied to clipboard
OCamlPro
OCamlPro public development repository for Alt-Ergo
The current implementation of `unsat_rec_prem` is wrong in presence of optimization if we try to use the SAT API directly. Consider the input problem: ```smt2 (set-option :produce-models true) (set-logic ALL)...
While implementing the `get-value` support (see #1032), I noticed that the decision level of `SatML` isn't always zero after calling `SAT.unsat`. It means we cannot always assert new facts after...
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)...
This umbrella issue tracks the progression of the BV theory reasoning. Please add related issue here and what we plan to improve in the future. - [X] Support of `bvnot`...
Please do not merge this PR on `next` before #789.
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...
I open this issue because I was trying to solve properly the issue #778 yesterday and I got stuck with the SAT solver API. We know that Alt-Ergo produces partial...
The following test have a different behavior given if the `push` instruction is here or not: File `test_adt.smt2` ``` (set-logic ALL) (declare-datatype t ((A) (B) (C (i Int)))) (declare-const e...
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...