Proof step 384 from proof inv-commit (previous step)

Heuristic symbolic execution applied rule if negative right

And obtained the following new goals

• Proof step 385:

  syn0 ↔ true, zh[rp] = mkznode(r, zbrar, boolvar, boolvar0, m), adr = adr3, adr0 = adr, err1 = err, ginval0 = ginval1, ginval4 = ginval0, gstore = gstore3, gstore0 = gstore4, gstore1 = gstore, gstore2 = gstore0, istore = istore3, istore0 = istore4, istore1 = istore, istore2 = istore0, maxino2 = maxino, pstate = readonly, remove-refsize0(gstore) = gstore, remove-refsize0(istore) = istore, remove-refsize0(gstore3) = gstore3, remove-refsize0(istore3) = istore3, elems nx ∩ ginval0 = ∅, dom remove-refsize0(gstore4) ∩ ginval1 = ∅, elems nx ∩ ginval1 = ∅, dom gstore ∪ elems nx = dom gstore0 ∪ ginval0, dom gstore3 ∪ elems nx = dom gstore4 ∪ ginval1, btree-inv(rp, adr3, istore4, istore3, zh, ri, fi), inv(gstore0 \ ginval0), inv(gstore), inv(istore0), inv(istore), inv(gstore4 \ ginval1), inv(gstore3), inv(istore4), inv(istore3), istore ⊑ istore0, istore3 ⊑ istore4, pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore0, pstate.index? → pstate.lnum ∈ istore0, ⌊err⌋ ∨ err = ESUCCESS ⊦ ⟪if false then {zh[rp].dirty := true; let maxino = 0 in {apersistence_get_iblock_refsize# (adr3.lnum, adr0, istore2, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate, syn0; ; maxino); apersistence_set_iblock_refsize# (adr3.lnum, maxino - adr3.size, adr0, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate, syn0; istore2)}}⟫ ( (∃ ri, fi. btree-inv(rp, adr0, istore2, istore1, zh, ri, fi)) ∧ inv(istore2) ∧ istore1 ⊑ istore2 ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore2) ∧ (pstate = unbuffered → syn0)), err1 = ESUCCESS, dups(nx), rp ≠ null ∧ boolvar0

Rule argument

Additional information