Basile Clément
Basile Clément
> Actually, we should always warn the user if we don't test the model, as there is no guarantee the model is sound (though I agree the model after timeout...
Following discussion at the users' club meeting: we should implement a soft timeout. The right place to check for the soft timeout is probably roughly where we increment the step...
Note that all these functions are handled using more generic propagators elsewhere. We might still want to consider specialized constant propagators for redundancy.
This is no longer a soundness bug since we explode distinct for now. Opened #1157 to track work on re-instating native support for distinct.
Works now.
Noting here something I noticed that might be useful when coming back to this issue: the implementation of `color` in `arith.ml` looks shady. ```ocaml let color ac = match ac.Sig.l...
Another note to self regarding #1172: this is maybe the wrong approach, because we still do different behavior depending on whether we have an AC-introduced constant for a top symbol...
(Taking over this one)
I have tried to follow the instructions to setup a flambda option on the Marvin bot but I get the following error on the `make _install` step: ``` File "middle_end/flambda2/parser/flambda_parser.ml",...
> configure: Configuring Flambda backend version 5.1.1+jst Ah! Probably I should not use the `main` branch :)