Boris Shingarov

I just tried to take another stab at it, and now the problem seems larger than I first thought. The "plain abstract refinements" (or to be precise, in what ICFP-15...

>getting sprite up-to-date with the latest fixpoint Yes, I have been following what's going on in the `bump-fixpoint` branch :-) >This above example requires "bounds" which sprite doesn't support at...

>at least on bump-fixpoint ... I am assuming also in yours? Yes, both that and the "more direct" `compose0x` work. Now everything makes perfect sense!!!

I am sorry for abusing your patience, I must be really dumb but there is still one corner of the ICFP-15 paper I still don't understand: the conclusion of the...

> the paragraph "Rule CApp" at the bottom of p6 that discusses this rule Yes, that paragraph is exactly what I can't understand. So we discard all the refinements —...

I took a fresh look at all this today, and now everything seems very easy! So we simply leave the arguments' refinements as κ-holes and let Horn inference find the...

> has extension .smt2 but the contents is not? These are the VCs passed down to `liquid-fixpoint`. One way to investigate what happens further down the pipeline, is to clone...

> `fixpoint test/L1/pos/.liquid/inc00.re.smt2 --save` > `$ cvc5 test/L1/pos/.liquid/inc00.re.smt2.smt2` > `(error "Parse Error: ...` This is a topic more suitable for discussing in `liquid-fixpoint`, because from Sprite's perspective, Sprite has generated...

Ping?

Let me take a look. No promises on when or even whether this will be fixed in a reasonable amount of time, but I'll at least investigate what's going on.