Basile Clément
Basile Clément
I don't understand why GitHub was saying there were merge conflicts in a bunch of files there were none? I force pushed again and that seems to have solved it.
Discussing with @Gbury and @Halbaroth we decided to try the following: Since one desirable effect of the weak table is for older terms to be sorted before younger terms *within...
I thought that this would only impact timeouts but... ```shell [nix-shell:~/Code/alt-ergo]$ ./src/bin/text/Main_text.exe --frontend dolmen /tmp/cos1.ae.zip -t 20 -o smtlib2 ; File "/tmp/cos1.ae.zip", line 2789, characters 1-93: Valid (0.4798) (8195 steps)...
We randomly made progress on this in #1025. Turns out that we use the "weak table" order to determine which variables to fix in the simplex, which can easily snowball...
Rebased on #1108
While investigating for #798 I realized that the Shostak cache should be mostly useless because most calls to `X.make` goes through the `Uf` module, and the `Uf` module maintains its...
Note: if theories create fresh names in `make`, having a global cache is useful to make sure that the same names are created in all environments. We used to do...
Yes, we won't have constraint simplification for 2.6. Let's keep it to track `bv2nat(bvadd)` support.
I wanted to implement support for `bv2nat` applied to `bvadd` etc. operators but did not find the time — or rather, I have several tentative implementations that need to be...
I said this but then realised we are not even able to prove that `(int2bv (+ (bv2nat x) (bv2nat y))` and `(bvadd x y)` are equal currently, so that's annoying....