[WIP] Update to use conditional elaboration

[clayrat]

Update to use ucsd-progsys/liquid-fixpoint#734

Don't merge yet, as the submodule is changed to point to a branch in a fork.

[clayrat]

[clayrat]

The performance charts were created before rebasing on top of #2482, so the discrepancy may be more pronounced than it really is. I will refresh them in a couple of hours.

[clayrat]

[nikivazou]

Great!!!!!! Are there tests running with cvc5? I am curious how the time compares between cvc5 and z3 :)

[clayrat]

The situtation with LH tests on CVC5 is not very straightforward, unfortunately. There are two issues at the moment:

• The PolySetBar test in the ple-pos group fails with an unknown func-sort error similar to PLE generates polymorphic applys for Sets #2438 (I am debugging this now)
• Some of the tests in the benchmark-bytestring group seem to trigger some pathological behaviour in cvc5, where the solver is left running at 100% CPU for several hours until the smtlib-backends-process API crashes with an Data.ByteString.hGetLine: end of file error.

If I exclude these two test groups, the performance seems comparable to Z3.

[clayrat]

Here are performance diffs comparing the CVC5 run excluding ple-pos and benchmark-bytestring (after) against the Z3 run (before). Both runs are done on the latest commit in this PR, i.e. d5aa806):