Pierre Villemot
Pierre Villemot
The SAT solver `CDCL` still produces model values for symbols that have been popped of the context. For instance this input file: ``` (set-option :produce-models true) (set-logic ALL) (declare-const x...
This issue is a remainder to rewrite the example `Lib_usage` after merging #1251. This module documented how to use the Alt-Ergo library with the legacy frontend. We cannot rewrite it...
While removing the legacy frontend, I ran our non regression test suite with the SAT solver `Tableaux`. I caught a bug. This test failed: ``` (set-logic ALL) (declare-fun P (Int)...
Consider the following input file (which is a polymorphic version of our `list.models.smt2`): ```smt2 (set-option :produce-models true) (set-logic ALL) (declare-datatypes ((List 1)) ( (par (T) ( (nil) (cons (head T)...
It seems we do not print definitions in models in the same order of the corresponding declarations in the input file. For instance, the following input: ```smt2 (set-option :produce-models true)...
This PR fixes the issue #929 about model arrays. Our implementation of `ArrayEx` is complete but we do not split on literals `a = b` where `a` and `b` are...
While trying to solve #1156, I took a look at our purification module in `Expr` and I suspect that this piece of code: https://github.com/OCamlPro/alt-ergo/blob/0d6300ec27446ea57626a19dc0a7b00a80daf3a7/src/lib/structures/expr.ml#L2799-L2817 is dead. Indeed, consider the input:...
We do not support timelimit and `:reproducible-resource-limit` on Windows because our implementation relies on Unix signals. We should support them using GC alarms as it does in Dolmen.
If I run `make dev-deps` in a project that requires a specific version of OCaml, drom will install all the dev dependencies in the current opam switch without checking that...