Open marcoeilers opened 3 months ago
For the following program, both backends report that len might not terminate:
len
field elem: Int field nxt: Ref predicate ll(r: Ref) { acc(r.elem) && acc(r.nxt) && (r.nxt != null ==> let rn == (r.nxt) in ll(rn)) } function len(r: Ref): Int requires ll(r) decreases ll(r) { unfolding ll(r) in (r.nxt == null ? 0 : 1 + len(r.nxt)) }
The program verifies if the let expression is removed and ll(rn) is replaced by ll(r.nxt).
let
ll(rn)
ll(r.nxt)
Reported by @Aurel300, found by a PV student.
For the following program, both backends report that
len
might not terminate:The program verifies if the
let
expression is removed andll(rn)
is replaced byll(r.nxt)
.Reported by @Aurel300, found by a PV student.