Pierre Villemot
Pierre Villemot
I used headache on my project but it seems to remove some lines. Let see a MRE: The header: ``` foo foo ``` The OCaml file: ``` (**************************************************************************) (* foo...
We don't manage correctly incremental type declarations. For instance the following input is accepted by the SMT-LIB standard: ```smt2 (set-logic ALL) (push 1) (declare-datatype t ((c1 (d1 Int)) (c2))) (pop...
The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`. This flag is important because the `Expr` AST doesn't store quantified type variables with binders as...
While looking for a minimal example that triggers a regression introduced by my patch in #1102, I ran into another issue (as always...) with our instantiation strategy. A relatively short...
Dolmen accepts to shadow some builtin types. For instance, the input file: ``` logic x : (int, int) farray type ('a, 'b) farray logic y : (int, int) farray goal...
The `next` branch raises an assertion on 23 tests of our internal benchmark set. We should fix this issue before releasing the next version of Alt-Ergo: ``` alt-ergo: option '--frontend':...
This PR removes the Record theory and sends all the records to the ADT theory. This modification does not fix #1008 as expected because SatML does not send some terms...
After refactoring both `Enum` and `ADT` theories, they shared most of their implementation. This PR merges `Enum` theory into `ADT` ones. This PR is rebased on #1093
If an input file contains custom built-in functions, Dolmen's binary cannot check the model as Dolmen's evaluation function doesn't know this built-in. For instance `Alt-Ergo` has a custom built-in `round`...
I was using Dolmen to check models generated by Alt-Ergo as follow: `alt-ergo --produce-models --frontend dolmen test.smt2 | dolmen --check-model true test.smt2` and I got the message: ``` File "",...