Basile Clément
Basile Clément
Same note as @Stevendeo, I cannot reproduce. This has probably been fixed sometime in the last 5 years, closing.
the test case in the issue is hidden by #731 but the underlying cause is probably still valid.
The assertion failure looks to be related to confusion in `intervalCalculus` about class representatives. The `intervalCalculus` environment is not consistent in the way it represents e.g. `ur_0 * ur_0`: sometimes...
> I don't think we should have polynomials with non-normalized terms lying around `--enable-assertions` confirms this: ```console $ alt-ergo --sat-solver CDCL --enable-assertions c_262_0_ae_bis.ae [Error]-ur_0'*'ur_0'*'ur_0+ur_0+109/50
Here is a simplified version that still exhibits the underlying cause (with `--enable-assertions`): ```alt-ergo logic ac f : real, real -> real function id_2() : real = 2. axiom ax_1:...
> The only thing that comes to mind is that with an AC symbol, `f(2, 1)` is not a subterm of `f(2, 1, 0)` and hence does not get picked...
The existing PSMT2 frontend is deprecated and will be replaced with the Dolmen frontend in the future. The Dolmen frontend already generates `Expr.t` directly (and can be in a way...
Closing as the GUI has been removed in #601
After #881 this would require: - If we have `a % b` and we learn that `b ≠ 0` (at least when we get `b > 0` or `b <...
This is somewhat expected because the definition for `length` gets expanded to: ```alt-ergo logic length : 'a t -> int axiom length_ext : forall list : 'a t. length(list) =...