Alex Gryzlov
Alex Gryzlov
> Much better! Let's merge! > > BTW, did you add a test that could not run before (i.e., was creating a crash) and passes now? I believe the feature...
Added a new test and inserted an additional coercion in LF (see https://github.com/ucsd-progsys/liquid-fixpoint/pull/696#issuecomment-2225652088), here are the new performance charts:   
The trouble is that all the generated constants and binds reference `Data.Map.Internal.Map @(0) int` (i.e., the underlying implementation) instead of `Bag_t @(0)` which then causes the LF elaborator to crash...
Added performance charts to https://github.com/ucsd-progsys/liquidhaskell/pull/2302. It seems we have significant slowdowns in ~5 tests, out of which `esop2013`, `bytestring`, `vector-algorithms` have large SMT encodings (10-100s Mb) and `ListSetDemo` is the...
I've added an environment coercion to `isUnsat` to fix an SMT serialization error triggered in the new test added to LH; I haven't encountered this in any other test before.
Yes, I thought about this a while ago, but the problem of default elements was exactly the showstopper I encountered – we either have to hardcode the default when creating...
> The situation here is identical to sets, right? That is, unions and intersections of sets are equally difficult to support in CVC5 (?). Actually, no - CVC5 has a...
When run with CVC5 1.2.0, this snippet produces the following error: `(error "Parse Error: test.smt2:16.39: Symbol 'as-array' not declared as a variable")`. I also couldn't find any references to `as-array`...
In `ByteString.Lazy` the problematic part of the code seems to be located in the [hGetContentsN](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/tests/benchmarks/bytestring-0.9.2.1/Data/ByteString/Lazy.hs#L1521), but the exact statement is hard to pinpoint, as minimizing the code seems to produce...
I've opened https://github.com/cvc5/cvc5/issues/11724 with the SMT2 file generated by `ByteString.Lazy`. In the end, I wasn't able to minimize this file in any meaningful way, either from the LH side (removing...