Status of the test case qf_shidlia_entl/dll-entl-05.smt2 and qf_shidlia_entl/dll-entl-13.smt2??

[ghost]

1. For the entailment qf_shidlia_entl/dll-entl-05.smt2, I rewrite it in the format of our prover Songbird as follows:

data RefDll_t {
    RefDll_t next;
    RefDll_t prev;
};

pred ldll(E,P,len1,F,L,len2) :=
    (emp & E=F & P=L & len1=len2)
    \/ (exists u,len3. E->RefDll_t{next:u,prev:P} *
        ldll(u,E,len3,F,L,len2) & len1=len3+1);

checkentail
ldll(E1,E1_prime,x1,E3,E3_prime,x3) *
ldll(E2,E2_prime,x2,E4,E4_prime,x4) *
ldll(E3,E3_prime,x3,E4,E4_prime,x4) *
ldll(E4,E4_prime,x4_prime,E3,E3_prime,x3_prime) *
ldll(E3,E3_prime,x3,E5,E5_prime,x5) *
ldll(E5,E5_prime,x5_prime,E3,E3_prime,x3_prime) *
ldll(E4,E4_prime,x4,E6,E6_prime,x6) & E2=E4 & E3=E5 |-
    ldll(E1,E1_prime,x1,E6,E6_prime,x6) *
    ldll(E4,E4_prime,x4_prime,E3,E3_prime,x3_prime);

Now, suppose that we unfold all predicates ldll(E1,E1_prime,x1,E3,E3_prime,x3) * ldll(E2,E2_prime,x2,E4,E4_prime,x4) * ldll(E3,E3_prime,x3,E4,E4_prime,x4) * ldll(E4,E4_prime,x4_prime,E3,E3_prime,x3_prime) * ldll(E3,E3_prime,x3,E5,E5_prime,x5) * ldll(E5,E5_prime,x5_prime,E3,E3_prime,x3_prime) * by their base case, except that last one ldll(E4,E4_prime,x4,E6,E6_prime,x6) to obtain a new entailment:

ldll(E5,E5_prime,x5_prime,E3,E3_prime,x3_prime) &
E1=E3 & E1_prime=E3_prime & x1=x3 &
E2=E4 & E2_prime=E4_prime & x2=x4 &
E3=E4 & E3_prime=E4_prime & x3=x4 &
E3=E5 & E3_prime=E5_prime & x3=x5 &
E4=E6 & E4_prime=E6_prime & x4=x6 &
E4=E3 & E4_prime=E3_prime & x4_prime=x3_prime & E2=E4 & E3=E5 |-
ldll(E1,E1_prime,x1,E6,E6_prime,x6) *
ldll(E4,E4_prime,x4_prime,E3,E3_prime,x3_prime);

which can be simplifed into:

ldll(E5,E5_prime,x5_prime,E5,E5_prime,x4_prime) |- 
ldll(E5,E5_prime,x2,E5,E5_prime,x2) * 
ldll(E5,E5_prime,x4_prime,E5,E5_prime,x4_prime)

According to their definition, the two predicates ldll(E5,E5_prime,x2,E5,E5_prime,x2) * ldll(E5,E5_prime,x4_prime,E5,E5_prime,x4_prime) in the RHS can only be unfolded by their base cases (otherwise, the induction case unfoldign will introduce E5!=E5, E5_prime!=E5_prime,x2!=x2..., which can be normalized to false)

Therefore, the previous entailment can be transformed into:

ldll(E5,E5_prime,x5_prime,E5,E5_prime,x4_prime) |-  emp

which is invalid, because there is no constraint correlate x5_prime and x4_prime, and the predicate in the LHS can be unfolded by the inductive case.

2. The same problem happns to the entailment qf_shidlia_entl/dll-entl-13.smt2:

data RefDll_t {
    RefDll_t next;
    RefDll_t prev;
};

pred ldll(E,P,len1,F,L,len2) := 
    (emp & E=F & P=L & len1=len2)
    \/ (exists u,len3. E->RefDll_t{next:u,prev:P} * ldll(u,E,len3,F,L,len2) & len1=len3+1);

checkentail
ldll(E1,E1_prime,x1,E3,E3_prime,x3) *
ldll(E2,E2_prime,x2,E4,E4_prime,x4) *
ldll(E3,E3_prime,x3,E4,E7,x4) *
ldll(E4,E4_prime,x4_prime,E3,E8,x3_prime) *
ldll(E3,E3_prime,x3,E5,E5_prime,x5) *
ldll(E5,E5_prime,x5_prime,E3,E9,x3_prime) *
ldll(E4,E4_prime,x4,E6,E6_prime,x6) &
E4_prime=E7 & E3_prime=E8 & E8=E9 |-
  ldll(E1,E1_prime,x1,E3,E3_prime,x3) *
  ldll(E2,E2_prime,x2,E6,E6_prime,x6);

By unfolding all predicates in the LHS, except the predciate ldll(E5,E5_prime,x5_prime,E3,E9,x3_prime), by their base case, we obtain the following entailment:

ldll(E5,E9,x5_prime,E5,E9,x4_prime) |- 
ldll(E5,E9,x6,E5,E9,x6) * 
ldll(E5,E9,x6,E5,E9,x6)

Here, heap predciates in their RHS can only be unfolded by base case to introduce the following entailment, which is invalid, because the LHS of the new entailment can be unfolded by the inductive case:

ldll(E5,E9,x5_prime,E5,E9,x4_prime) |- emp

[zhilin02]

Hi tddsg,

We checked the two benchmarks manually as well. As you said, the results for dll-entl-05.smt2 and dll-entl-13.smt2 should be sat, namely, the entailment does not hold. There were a bug in the implementation of Comp-Spen. Thank you for pinpointing this.

[slcomp]

Fixed on the GitHub.