Analysis of entailments with issues about hipsleek HOT 24 OPEN

The following table compares results of ./sleek -dre="compute_pretty_actions\|isFailCtx" --pnum <pnum> <filename> | ./remove-aliases.py | less for <pnum>s 14 and 15, at commit 5edb3fc.

If table is too wide, please scroll horizontally.

<pnum> 14 is valid.
The row of <pnum> 15 is identical to the one in the first table above.

The chosen function@call for <pnum> 14 is the only function@call in the entire result of 14 to have an analogous entailment to the entailment of the function@call of <pnum> 15.

It seems from this comparison that if <pnum> 15 was able to either indirectly unfold int_arr_seg<1> into arr_seg<4>, or do so directly via lemma "int2char", then a subsequent Match action would make the <pnum> 15 valid.

from hipsleek.

The following table shows results of ./sleek -dre="compute_pretty_actions\|isFailCtx" --pnum <pnum> <filename> | ./remove-aliases.py | less, at commit bfc0a33.

If table is too wide, please scroll horizontally.

from hipsleek.

Merge of two tables at #1 (comment) and #1 (comment), with updated indexes as in c00c0bd. The results of #1 (comment) have merely been copied, and have not been reproduced at commit c00c0bd.

Comments of #1 (comment) are appended with, whenever they are relevant to the row:

1. a comment on search actions, and
2. a comment on unprovable formulae due to some variable not being universally quantified.

If table is too wide, please scroll horizontally.

from hipsleek.

At commit c00c0bd, ./sleek testcases/ex5c.slk gives Unexpected List: [24,25,33,34,35,37,38,40,41]. In contrast, invoking ./sleek --pnum <pnum> testcases/ex5c.slk for <pnum> in range 1 to 57, so that ./sleek --pnum 24 testcases/ex5c.slk gives Unexpected List: [24], the <pnum>s that give Unexpected Lists are: 24,25,26,29,30,31,33,34,35,37,38,40,41,42,43,44,45,47,48,49,50,51,53.

A similar analysis shows no difference in unexpected entailments for exist-arrays.slk. That is, ./sleek testcases/exist-arrays.slk gives Unexpected List: [18,25,30,31], and ./sleek --pnum <pnum> testcases/ex5c.slk for <pnum> in range 1 to 31, the <pnum>s that give Unexpected Lists are: 18,25,30,31.

Could be related to hipsleek#30.

from hipsleek.

I modified the lemmas "splitchar" and "splitint", and observed the Unexpected List given by ./sleek testcases/ex5c.slk.

The first row has "splitchar" and "splitint" as in 5ddd4c3.
The second row has "splitchar" and "splitint" as in 5ddd4c3, but a>=0 & b>=0 is added to the LHS.
The third row has "splitchar" and "splitint" as in 5ddd4c3, but a>0 & b>0 is added to the LHS.

[   24,25,26,   29,30,31,   33,34,35,   37,38,   40,41,42,43,44,45,   47,48,49,50,51,   53]
[   24,25,26,   29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,NA,NA,NA,NA,NA,NA,NA,NA]
[22,24,25,   27,29,30,   32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53]

The second row was left to run for 10 minutes, but was still stuck at entailment 45, so all later entailments are marked as NA.

The first and second rows should not differ, since the lemmas as in the second row can be derived from the lemmas as in the first row: consider the lemmas as in the first row. Both a>=0, b>=0 are given by arr_seg<a>, arr_seg<b> in the RHS. Then, because variables a, b are in the LHS too, we can move both a>=0, b>=0 to the LHS. So, the lemmas are as in the second row.

from hipsleek.

At commit f941e6f, the important differences between testcases/ex5c.slk.geq and testcases/ex5c.slk.geqno.subst (i.e. ignoring 0<=a_315 & 0<=b_316 and the ordering of commutative operators like &) are:

1. testcases/ex5c.slk.geqno.subst:237: a_315=4*flted_307_304
2. testcases/ex5c.slk.geq:244: es_pure: flted_16_310=4*flted_307_304
3. testcases/ex5c.slk.geq:291: 0<=flted_306_285
4. testcases/ex5c.slk.geq:292: 0<=5
5. testcases/ex5c.slk.geqno.subst:334: a_315=4*flted_307_304
6. testcases/ex5c.slk.geqno.subst:336: 4*flted_307_304=4*1 & 4*flted_307_304+x=q_314 & 5=b_316+4*flted_307_304

And also, the rest of the two files are completely different.

The below table shows, for each function@call, the traversed search path that I deduced from reading testcases/ex5c.slk.geqno.subst. The traversed search path for compute_pretty_actions excludes the subpath printed at EXIT. The traversed search path for do_match is the path printed at es_trace.

I write out the full call stack "call" in function@call, e.g. compute_pretty_actions@8@7, since this indicates that the function higher in the call stack do_match@7 uses compute_pretty_actions@8@7 to traverse the search path till the action UnmatchedRHSData, and subsequently EXIT with a MaybeErr because of do_unmatched_rhs.

The first compute_pretty_actions, compute_pretty_actions@1, is syntactically identical to the original entailment, except with aliases. As such, there is no traversed search path.

By analyzing the entailments at each function@call, I deduce do_match@10 as the final action. This corresponds with the final traversed search path, [[ SEARCH ==> SEARCH ==> (Lemma <== int2char_left_right(x,x)) ==> SEARCH ==> SEARCH ==> (Lemma ==> splitchar_left(x,x)) ==> SEARCH ==> COND ==> Match(x,x) ==> SEARCH ==> SEARCH ==> COND ==> Match(q_314,y)]]. Then, the chain of "function@call"s leading to validity is: compute_pretty_actions@1 ==> compute_pretty_actions@2 ==> compute_pretty_actions@4 ==> do_match@5 ==> compute_pretty_actions@9 ==> do_match@10.

Correspondingly, the below table shows, for each function@call, the traversed search path that I deduced from reading testcases/ex5c.slk.geq. Since all rows up to compute_pretty_actions@9 are nearly identical, they have been omitted.

The final traversed search path is [[ SEARCH ==> SEARCH ==> (Lemma <== int2char_left_right(x,x)) ==> SEARCH ==> SEARCH ==> (Lemma ==> splitchar_left(x,x)) ==> SEARCH ==> COND ==> Match(x,x) ==> SEARCH ==> COND ==> UnmatchedRHSData]], and the chain of "function@call"s leading to failure is: compute_pretty_actions@1 ==> compute_pretty_actions@2 ==> compute_pretty_actions@4 ==> do_match@5 ==> compute_pretty_actions@9.

It appears testcases/ex5c.slk.geq fails because this is compute_pretty_actions@9's EXIT:

SEARCH =>[
  Prio:2
  COND =>[
   Prio:2
   BaseCaseFold =>
     Type: Root
     LHS: emp
     RHS: y::arr_seg<flted_307_303>@M
     root_inst: None
     lhs_rest: q_314::arr_seg<b_316>@M
     rhs_rest: emp
     alias set: []rhs_inst: []rhs_infer: None;
   Prio:5
   UnmatchedRHSData =>  y::arr_seg<flted_307_303>@M
   ]
   ]

as compared to testcases/ex5c.slk.geqno.subst's compute_pretty_actions@9's EXIT:

SEARCH =>[
  Prio:1
  SEARCH =>[
   Prio:1
   COND =>[
    Prio:1
    Match =>
      Type: Root
      LHS: q_314::arr_seg<b_316>@M
      RHS: y::arr_seg<flted_307_303>@M
      root_inst: None
      lhs_rest: emp
      rhs_rest: emp
      alias set: [q_314,y]rhs_inst: []rhs_infer: None;
    Prio:3
    COND =>[
     Prio:3
     BaseCaseFold =>
       Type: Root
       LHS: q_314::arr_seg<b_316>@M
       RHS: y::arr_seg<flted_307_303>@M
       root_inst: None
       lhs_rest: emp
       rhs_rest: emp
       alias set: [q_314,y]rhs_inst: []rhs_infer: None;
     Prio:3
     BaseCaseUnfold =>
       Type: Root
       LHS: q_314::arr_seg<b_316>@M
       RHS: y::arr_seg<flted_307_303>@M
       root_inst: None
       lhs_rest: emp
       rhs_rest: emp
       alias set: [q_314,y]rhs_inst: []rhs_infer: None
     ]
     ];
    Prio:1
    (Lemma 0==> splitchar_left) =>
      Type: Root
      LHS: q_314::arr_seg<b_316>@M
      RHS: y::arr_seg<flted_307_303>@M
      root_inst: None
      lhs_rest: emp
      rhs_rest: emp
      alias set: [q_314,y]rhs_inst: []rhs_infer: None;
    Prio:1
    (Lemma 0<== splitchar_left_right) =>
      Type: Root
      LHS: q_314::arr_seg<b_316>@M
      RHS: y::arr_seg<flted_307_303>@M
      root_inst: None
      lhs_rest: emp
      rhs_rest: emp
      alias set: [q_314,y]rhs_inst: []rhs_infer: None
    ]
    ]

So it appears that one of important differences at the start of this comment is related to compute_pretty_actions@9's EXIT:
5. testcases/ex5c.slk.geqno.subst:334: a_315=4*flted_307_304

The entailments corresponding to function calls in testcases/ex5c.slk.geqno.subst is:

from hipsleek.

At commit 9d6ecf4, the important differences between testcases/ex5c.slk.trace-log-num_5.geq and testcases/ex5c.slk.trace-log-num_5.geqno.subst (i.e. ignoring 0<=a_315 & 0<=b_316 and the ordering of commutative operators like &) are listed below. This list is non-exhaustive, and may be made exhaustive with further efforts.

1. testcases/ex5c.slk.trace-log-num_5.geq:382-385 has

   @5!:0: 0: **tpdispatcher.ml#3745:new_conseq: exists(b_316:exists(a_315:exists(q_314:flted_306_285=b_316+a_315 & 
                                           a_315+x=q_314 & 0<=a_315 & 
                                           0<=b_316 & flted_306_285=5 & y=
                                           4+x & a_315=4*flted_307_304)))
   

   whereas testcases/ex5c.slk.trace-log-num_5.geqno.subst:382-385 has

   @5!:0: 0: **tpdispatcher.ml#3745:new_conseq: exists(q_314:exists(a_315:exists(b_316:flted_306_285=b_316+a_315 & 
                                           a_315+x=q_314 & flted_306_285=5 & 
                                           y=4+x & a_315=4*flted_307_304)))
   @5! **cpure.ml#2981:vs(mkExists):[b_316]
   

   So, the only important difference is the order of the existential quantifiers. There is also some difference in the lines after:

   @5! **cpure.ml#2981:vs(mkExists):
   @5! **cpure.ml#2982:vs(filtered rel type):
   

2. testcases/ex5c.slk.trace-log-num_5.geq:392-395 has

   @5! **omega.ml#901:simplify_ops_x(after trans_arr)::
    exists(b_316:0<=b_316 & flted_306_285=5 & y=4+x & 
                 flted_306_285=b_316+(4*flted_307_304) & 0<=(4*flted_307_304))
   @5! **omega.ml#454:omega inp:{[y, x, flted_306_285, flted_307_304] : ( (exists (b_316:((((0 <= b_316) & (flted_306_285 = 5)) & (y = 4 + x)) & ((flted_306_285 = b_316 + 4(flted_307_304)) & (0 <= 4(flted_307_304)))))) )};
   

   whereas testcases/ex5c.slk.trace-log-num_5.geqno.subst:393-397 has

   @5! **omega.ml#901:simplify_ops_x(after trans_arr)::
    exists(q_314:flted_306_285=5 & y=4+x & 
                 exists(b_316:flted_306_285=b_316+(4*flted_307_304) & 
                              (4*flted_307_304)+x=q_314))
   @5! **omega.ml#454:omega inp:{[y, flted_306_285, flted_307_304, x] : ( (exists (q_314:(((flted_306_285 = 5) & (y = 4 + x)) &  (exists (b_316:((flted_306_285 = b_316 + 4(flted_307_304)) & (4(flted_307_304) + x = q_314)))) ))) )};
   

from hipsleek.

I believe a_315=4*flted_307_304 may not be derived in the antecedent when lemmas have a >=0 & b >= 0 as in commit 2649b4e, precisely because flted_307_304 ranges over the integers, and a_315=4*flted_307_304 is not satisfiable when a ranges over the naturals, e.g. when flted_307_304 is negative.

from hipsleek.

Entailment 32 of ex5c.slk was investigated at commit 9d6ecf4, that is, checkentail x::arr_seg<5> & y=x+4 |- x::int_arr_seg<1> * y::arr_seg<1>.. It was found that replacing int_arr_seg with arr_seg made the entailment valid, that is, checkentail x::arr_seg<5> & y=x+4 |- x::arr_seg<4> * y::arr_seg<1>. is valid. So, a small example, file.slk, was crafted to figure out why lemma "int2char" was failing:

data ch_star{
    int val;
}.

pred arr_seg<n>     == self::ch_star<_> & n=1
                    or self::ch_star<_> * q::arr_seg<n-1> & q=self+1 & n>1
  inv n>=1.

pred int_arr_seg<n> == self::ch_star<_> * x::ch_star<_> & x=self+1 & n=1
                    or self::ch_star<_> * x::ch_star<_> * q::int_arr_seg<n-1> & x=self+1 & q=x+1 & n>1
  inv n>=1.

lemma_unsafe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n.

checkentail x::int_arr_seg<n> & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<_> * q::arr_seg<m-1>.
print residue.
expect Valid.

where int_arr_seg is now defined as two adjacent ch_stars, and the entailment is the same as lemma "int2char", but with the right hand side folded once. On invoking ./sleek -dre="compute_actions\|do_match" --trace-log-num 8 file.slk, the search strategy is [[ SEARCH ==> Unfold 0 ==> SEARCH ==> Match(x,x) ==> SEARCH ==> Fold ==> SEARCH ==> Match(x_145,q)]], which unfolds x::int_arr_seg into x::ch_star and x_145::ch_star and q_147::int_arr_seg, then a match on xs, then a folding on q::arr_seg into q::ch_star and q_150::arr_seg, then match on x_145 and q, then fails at applying the inductive hypothesis (i.e. fails at applying the lemma defined with smaller predicates) on q_147::int_arr_seg and q_150::arr_seg.

The inductive lemma was split up into its base case and inductive case, which theoretically makes debugging easier:

//lemma_unsafe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n.
lemma_unsafe "base" self::int_arr_seg<1> <- self::arr_seg<2>.
lemma_unsafe "inductive" self::int_arr_seg<n> & m=2*n & n>1 <- self::arr_seg<m>.

On invoking ./sleek -dre="compute_actions\|do_match" --trace-log-num 8 file.slk (side note: this generates different variable names), it was noticed that do_match@8 has as error cond action is empty. So, it was conjectured that applying the inductive hypothesis fails because q_167::int_arr_seg and q_170::arr_seg are not aliased. The alias q_167=q_170 should be derivable from q_167=1+x_165 & x_165=q & q_170=1+q, but then the alias x_165=q does not exist. So, let add_to_lhs = (CP.mkEqVar lhs_self rhs_self no_pos) :: add_to_lhs in was added to do_match_x in solver.ml, so that x_165=q is aliased.

To check that q_167=q_170 is indeed derivable from q_167=1+x_165 & x_165=q & q_170=1+q, it was checked that checkentail q_167::ch_star<_> & q_167=1+x_165 & x_165=q |- q_170::arr_seg<_> & q_170=1+q. is valid, and it is, with a Match(q_167,q_170) being performed, indicating the two locations are aliased.

Since all the prerequisites to applying the inductive hypothesis have been satisfied, the only remaining obstacle is the actual application of the inductive hypothesis. To debug this, the proof tree was derived manually, and the following manual derivation was confirmed to be identical to the proof tree in the output of ./sleek -dre="compute_actions\|do_match" file.slk, with each line of the derivation corresponding to the function@call commented at the end of the line, and the action taken to derive the line at the end of the line:

// checkentail x::int_arr_seg<n> & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<Anon_18> * q::arr_seg<m-1>. // compute_actions@1 []
// checkentail x::ch_star<Anon_166> * x_167::ch_star<Anon_168> * q_169::int_arr_seg<n-1> & x_167=x+1 & q_169=x_167+1 & n>1 & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<Anon_18> * q::arr_seg<m-1>. // compute_actions@2 [Unfold]
// checkentail x_167::ch_star<Anon_168> * q_169::int_arr_seg<n-1> & x_167=x+1 & q_169=x_167+1 & n>1 & m=2*n & n>1 & q=x+1 & m>1 & Anon_18=Anon_166 |- q::arr_seg<m-1>. // compute_actions@4 [Match]

// checkentail x_167::ch_star<Anon_168> * q_169::int_arr_seg<n-1> & x_167=x+1 & q_169=x_167+1 & n>1 & m=2*n & n>1 & q=x+1 & m>1 & Anon_18=Anon_166 |- q::ch_star<Anon_170> & m-1=1. // compute_actions@5 [Fold (base case)]
// checkentail q_169::int_arr_seg<n-1> & x_167=x+1 & q_169=x_167+1 & n>1 & m=2*n & n>1 & q=x+1 & m>1 & Anon_18=Anon_166 & Anon_168=Anon_170 |- m-1=1. // [Match]
// (must-bug) 1<=n-1 & 1<(n-1+1) & 1<m & m=n-1+1+n-1+1 |-  1+1=m.

// checkentail x_167::ch_star<Anon_168> * q_169::int_arr_seg<n-1> & x_167=x+1 & q_169=x_167+1 & n>1 & m=2*n & n>1 & q=x+1 & m>1 & Anon_18=Anon_166 |- q::ch_star<Anon_171> * q_172::arr_seg<m-1-1> & q_169=q+1 & m-1>1. // compute_actions@7 [Fold (inductive case)]
// checkentail q_169::int_arr_seg<n-1> & x_167=x+1 & q_169=x_167+1 & n>1 & m=2*n & n>1 & q=x+1 & m>1 & Anon_18=Anon_166 & Anon_168=Anon_170 |- q_172::arr_seg<m-1-1> & q_172=q+1 & m-1>1. // compute_actions@9 [Match]
// [NothingToDo]

The proof tree splits into two at action [Fold], since one branch has the base case in the consequent, and the other branch has the inductive case in the consequent.

It is expected (?) that the branch with the base case ends with (must-bug), because the [Unfold] action at function@call compute_actions@2 unfolds the predicate to become the inductive case. So, the array segment in the antecedent is longer than the array segment in the consequent, by at least one inductive step. Because the array predicates use constraints on the array sizes, the constraints in the antecedent are connected to the constraints in the consequent. Because the array sizes are different, there is no way the entailment can be valid. On the other hand, if the [Unfold] action at function@call compute_actions@2 unfolds the predicate to become the base case, the entailment should be valid.

It is unexpected that the branch with the inductive case ends with action [NothingToDo], since although the line of the derivation corresponding to the last function@call, compute_actions@9, has a similar form to checkentail q_169::ch_star<_> & q_169=1+x_167 & x_167=q |- q_172::arr_seg<_> & q_172=1+q. from which hipsleek knows q_169=q_172, the line of the derivation does not have an identical form. Specifically, the data predicates are different. So, it could be that checkentail q_169::int_arr_seg<n-1> & x_167=q & q_169=x_167+1 & n>1 & m=2*n & n>1 & m>1 |- q_172::arr_seg<m-1-1> & q_172=q+1 & m-1>1. is invalid, and hipsleek does not know that q_169=q_172, and the induction hypothesis cannot be applied.

Analyzing this further, it is found that although checkentail q::int_arr_seg<1> |- q::ch_star<_> * r::ch_star<_> & r=q+1. and checkentail q::arr_seg<2> |- q::ch_star<_> * r::ch_star<_> & r=q+1. are valid, checkentail q::int_arr_seg<1> |- q::arr_seg<2>. is invalid with Fail_May, and last action NothingToDo. To make this entailment valid, a lemma lemma "obvious" self::int_arr_seg<1> -> self::arr_seg<2>. was introduced.

Continuing this train of thought, lemma "obvious" was generalized to all array sizes, lemma "obvious" self::int_arr_seg<n> & m=2*n -> self::arr_seg<m>.. Then, checkentail q_169::int_arr_seg<n-1> & x_167=q & q_169=x_167+1 & n>1 & m=2*n & n>1 & m>1 |- q_172::arr_seg<m-1-1> & q_172=q+1 & m-1>1. becomes valid. So applying the induction hypothesis is now possible. And indeed, with the generalized lemma "obvious", the original entailment in the crafted small example checkentail x::int_arr_seg<n> & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<_> * q::arr_seg<m-1>. becomes valid, see the inlined file:

data ch_star{
    int val;
}.

pred arr_seg<n>     == self::ch_star<_> & n=1
                    or self::ch_star<_> * q::arr_seg<n-1> & q=self+1 & n>1
  inv n>=1.

pred int_arr_seg<n> == self::ch_star<_> * x::ch_star<_> & x=self+1 & n=1
                    or self::ch_star<_> * x::ch_star<_> * q::int_arr_seg<n-1> & x=self+1 & q=x+1 & n>1
  inv n>=1.

lemma "obvious" self::int_arr_seg<n> & m=2*n -> self::arr_seg<m>.
//lemma_unsafe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n.
lemma_unsafe "base" self::int_arr_seg<1> <- self::arr_seg<2>.
lemma_unsafe "inductive" self::int_arr_seg<n> & m=2*n & n>1 <- self::arr_seg<m>.

checkentail x::int_arr_seg<n> & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<_> * q::arr_seg<m-1>.
print residue.
expect Valid.

from hipsleek.

The analysis in #1 (comment) is misguided. Since entailment 32 of ex5c.slk at commit 9d6ecf4, checkentail x::arr_seg<5> & y=x+4 |- x::int_arr_seg<1> * y::arr_seg<1>., is invalid, whereas checkentail x::arr_seg<5> & y=x+4 |- x::arr_seg<4> * y::arr_seg<1>. is valid, then the investigation should have analyzed folding the int_arr_seg to become a arr_seg.

With this in mind, the lemma lemma_unsafe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n. does perform a folding. However, the entailment checkentail x::int_arr_seg<n> & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<_> * q::arr_seg<m-1>. does not expect a folding to be performed! The entailment expects an Unfold on int_arr_seg to become a arr_seg. The conclusion in that comment is: lemma "obvious" that forces Unfolding of int_arr_seg to become a arr_seg makes the entailment valid. Of course!

Here is the corrected version of the example in that comment. Here, the lemma lemma "int2char" is now an unfolding lemma, and so the entailment is valid.

data ch_star{
    int val;
}.

pred arr_seg<n>     == self::ch_star<_> & n=1
                    or self::ch_star<_> * q::arr_seg<n-1> & q=self+1 & n>1
  inv n>=1.

pred int_arr_seg<n> == self::ch_star<_> * x::ch_star<_> & x=self+1 & n=1
                    or self::ch_star<_> * x::ch_star<_> * q::int_arr_seg<n-1> & x=self+1 & q=x+1 & n>1
  inv n>=1.

lemma_safe "int2char" self::int_arr_seg<n> -> self::arr_seg<m> & m=2*n.

checkentail x::int_arr_seg<n> & m=2*n & n>1 & q=x+1 & m>1 |- x::ch_star<_> * q::arr_seg<m-1>.
print residue.
expect Valid.

It should be noted that lemma_safe "int2char" is valid.

Analysis of lemma "int2char" as a folding lemma is deferred to a later comment.

from hipsleek.

As per the defect of #1 (comment) highlighted in #1 (comment), we now investigate the folding lemma lemma_safe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n., which, when checked for safety, gives Entailing lemma int2char: Fail. (cex)(may) cause: OrL[residue is forbidden.(1), valid].

As in #1 (comment), we split the failing lemma into the base case and inductive case. Since splitting the lemma actually impacts the proof search now, we elaborate more on the two cases. As expected, the base case lemma_safe "base" self::int_arr_seg<1> <- self::arr_seg<2>. is valid. However, the inductive case lemma_safe "inductive" self::int_arr_seg<n> & m=2*n & n>1 <- self::arr_seg<m>. is invalid, failing with Entailing lemma inductive: Fail. (cex)(must) cause: residue is forbidden.(1).

Then, it was checked that under all these lemmas, checkentail x::arr_seg<m> & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::int_arr_seg<n>. is valid, which it is. The proof search is a single application of lemma "inductive", followed by a single Match.

Then, int_arr_seg was manually folded to give checkentail x::arr_seg<m> & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::ch_star<_> * q::ch_star<_> * r::int_arr_seg<n-1>.. This prevents direct application of lemma "inductive" as before. The expected proof search here is 2 Unfolds on arr_seg, then 2 Matches on the ch_stars, then the application of the inductive hypothesis. The example file, file.slk, is:

data ch_star{
    int val;
}.

pred arr_seg<n>     == self::ch_star<_> & n=1
                    or self::ch_star<_> * q::arr_seg<n-1> & q=self+1 & n>1
  inv n>=1.

pred int_arr_seg<n> == self::ch_star<_> * x::ch_star<_> & x=self+1 & n=1
                    or self::ch_star<_> * x::ch_star<_> * q::int_arr_seg<n-1> & x=self+1 & q=x+1 & n>1
  inv n>=1.

//lemma_unsafe "int2char" self::int_arr_seg<n> & m=2*n <- self::arr_seg<m>.
lemma_unsafe "base" self::int_arr_seg<1> <- self::arr_seg<2>.
lemma_unsafe "inductive" self::int_arr_seg<n> & m=2*n & n>1 <- self::arr_seg<m>.

checkentail x::arr_seg<m> & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::ch_star<_> * q::ch_star<_> * r::int_arr_seg<n-1>.
print residue.
expect Valid.

The proof tree for ./sleek --pprint -dre="compute_actions\|do_match" file.slk is:

// checkentail x::arr_seg<m> & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::ch_star<Anon_18> * q::ch_star<Anon_19> * r::int_arr_seg<n-1>. // compute_actions@1 []
// checkentail x::ch_star<Anon_158> * q_159::arr_seg<m-1> & q_159=x+1 & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::ch_star<Anon_18> * q::ch_star<Anon_19> * r::int_arr_seg<n-1>. // compute_actions@2 [Unfold]
// checkentail q_159::arr_seg<m-1> & q_159=x+1 & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- q::ch_star<Anon_19> * r::int_arr_seg<n-1>. // compute_actions@4 [Match]
// checkentail q_159::ch_star<Anon_171> * q_172::arr_seg<m-1-1> & q_172=q_159+1 & q_159=x+1 & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- q::ch_star<Anon_19> * r::int_arr_seg<n-1>. // compute_actions@5 [Unfold]
// checkentail q_172::arr_seg<m-1-1> & q_172=q_159+1 & q_159=x+1 & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- r::int_arr_seg<n-1>. // compute_actions@7 [Match]
// checkentail q_172::arr_seg<m-1-1> & q_172=q_159+1 & q_159=q & m=2*n & n>1 & r=q+1 & m>1 |- r::arr_seg<m_176> & m_176=n-1+n-1. // compute_actions@8 [lemma "inductive"]
// checkentail q_172::arr_seg<m-1-1> & q_172=q_159+1 & q_159=x+1 & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- r::arr_seg<2>. // compute_actions@10 [lemma "base"]

After compute_actions@8, do_match@9 fails. Further investigation reveals that checkentail q_172::arr_seg<flted_6_170> & flted_6_170+1=flted_6_157 & q_172=1+q_159 & 1<flted_6_157 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_159=1+x & flted_6_157+1=m |- r::arr_seg<n-1+n-1> & 1<n-1. is invalid, but removing 1<n-1 from the consequent makes the entailment valid (that is, checkentail q_172::arr_seg<flted_6_170> & flted_6_170+1=flted_6_157 & q_172=1+q_159 & 1<flted_6_157 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_159=1+x & flted_6_157+1=m |- r::arr_seg<n-1+n-1>. is valid). This is because 1<n-1 cannot be proven from 1<n, since checkentail n>1 |- n>2. is invalid with Fail_May. Therefore the lemma lemma "inductive" cannot have the boolean guard n>1, neither in its antecedent, nor in its consequent. Here is the updated file.slk:

data ch_star{
    int val;
}.

pred arr_seg<n>     == self::ch_star<_> & n=1
                    or self::ch_star<_> * q::arr_seg<n-1> & q=self+1 & n>1
  inv n>=1.

pred int_arr_seg<n> == self::ch_star<_> * x::ch_star<_> & x=self+1 & n=1
                    or self::ch_star<_> * x::ch_star<_> * q::int_arr_seg<n-1> & x=self+1 & q=x+1 & n>1
  inv n>=1.

//lemma_unsafe "int2char" self::int_arr_seg<n> & m=2*n <- self::arr_seg<m>.
lemma_unsafe "base" self::int_arr_seg<1> <- self::arr_seg<2>.
lemma_unsafe "inductive" self::int_arr_seg<n> & m=2*n <- self::arr_seg<m>.

checkentail x::arr_seg<m> & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::ch_star<Anon_18> * q::ch_star<Anon_19> * r::int_arr_seg<n-1>.
print residue.
expect Valid.

Despite this, do_match@9 still fails. Further investigation reveals that checkentail q_170::arr_seg<flted_6_168> & flted_6_168+1=flted_6_155 & q_170=1+q_157 & 1<flted_6_155 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_157=1+x & flted_6_155+1=m |- r::arr_seg<m_174> & m_174=flted_17_144+flted_17_144. is invalid, but adding either flted_17_144+1=n or flted_6_168=flted_17_144+flted_17_144 to the antecedent makes the entailment valid (that is, both checkentail q_170::arr_seg<flted_6_168> & flted_6_168+1=flted_6_155 & q_170=1+q_157 & 1<flted_6_155 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_157=1+x & flted_6_155+1=m & flted_17_144+1=n |- r::arr_seg<m_174> & m_174=flted_17_144+flted_17_144. and checkentail q_170::arr_seg<flted_6_168> & flted_6_168+1=flted_6_155 & q_170=1+q_157 & 1<flted_6_155 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_157=1+x & flted_6_155+1=m & flted_6_168=flted_17_144+flted_17_144 |- r::arr_seg<m_174> & m_174=flted_17_144+flted_17_144. are valid).

In other words, these additions to the antecedent "connect the array sizes" on both the antecedent and the consequent, allowing Match. This means additions to the antecedent that only reason about array sizes on the antecedent, like flted_6_168=n-1+n-1, do not make the entailment valid (that is, checkentail q_170::arr_seg<flted_6_168> & flted_6_168+1=flted_6_155 & q_170=1+q_157 & 1<flted_6_155 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_157=1+x & flted_6_155+1=m & flted_6_168=n-1+n-1 |- r::arr_seg<m_174> & m_174=flted_17_144+flted_17_144. is invalid).

But here is an exception: although flted_168=m_174 "connects the array sizes" on both the antecedent and the consequent, adding flted_168=m_174 to the antecedent does not make the entailment valid (that is, checkentail q_170::arr_seg<flted_6_168> & flted_6_168+1=flted_6_155 & q_170=1+q_157 & 1<flted_6_155 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_157=1+x & flted_6_155+1=m & flted_6_168=m_174 |- r::arr_seg<m_174> & m_174=flted_17_144+flted_17_144. is invalid).

Investigating array sizes, it seems like removing the constraint that m_174 is even, that is, removing m_174=flted_17_144+flted_17_144 from the consequent, makes the enatilment valid (that is, checkentail q_170::arr_seg<flted_6_168> & flted_6_168+1=flted_6_155 & q_170=1+q_157 & 1<flted_6_155 & m=n+n & 1<n & q=1+x & r=1+q & 1<m & q_157=1+x & flted_6_155+1=m |- r::arr_seg<m_174>. is valid).

To simplify further investigation, the inductive case entailment after action lemma "inductive" was applied is simplified to checkentail r::arr_seg<m-1-1> & m=n+n & n>1 & m>2 |- r::arr_seg<m_174> & m_174=flted_17_144+flted_17_144., which is invalid.

Similarly, the base case entailment after action lemma "base" was applied is simplified to checkentail r::arr_seg<m-1-1> & m=2*n & n>1 & m>2 |- r::arr_seg<2>., which is invalid. Adding n=2 to the antecedent makes the base case entailment valid (that is, checkentail r::arr_seg<m-1-1> & m=n+n & n>1 & m>2 & n=2 |- r::arr_seg<2>. is valid). Investigating further, running hipsleek on the simplified base case entailment gives r::arr_seg<flted_22_122> & 2<m & 1<n & m=n+n & flted_22_122+1+1=m |- r::arr_seg<flted_22_144> & flted_22_144=2, and looking at fc_message (1<n & 2<(n+n) & (((2<=flted_22_122 & r!=null) | (flted_22_122=1 & r!=null))) & flted_22_122+1+1=n+n |- flted_22_122=2.), we know that hipsleek case-split flted_22_122 into flted_22_122=1 and flted_22_122>=2. This is an acceptable proof strategy. Clearly, flted_22_122=1 cannot prove flted_22_122=2. Therefore, we require the condition that flted_22_122!=1, or in terms of the simplified base case entailment, m-1-1!=1. But we already have this from m>2 and m=n+n: from m>2 we know m>=3, and from m>=3 and m=n+n we know m>=4, and checkentail m>=4 |- m-1-1!=1. is valid. Notably, m-1-1!=1 is not derivable from m>2 alone. That is, the knowledge that m is even is important.

from hipsleek.

Comment #1 (comment) hinted strongly that, for both the base and inductive cases, knowledge that some variable is even is important. However, the comment's analysis of the base case is incomplete.

The simplified base case entailment is checkentail r::arr_seg<m-1-1> & m=2*n & n>1 & m>2 |- r::arr_seg<2>.. It was correctly identified in the comment that m-1-1!=1 is required to exclude the case where m-1-1=1. However, !(m-1-1>2) is also required to exclude the case where m-1-1>2, because checkentail m-1-1>=2 |- m-1-1=2. is invalid with Fail_May, while checkentail m-1-1>=2 & !(m-1-1>2) |- m-1-1=2. is valid.

Indeed, checkentail r::arr_seg<m-1-1> & m=n+n & n>1 & m>2 & !(m-1-1>2) |- r::arr_seg<2>. is valid. In other words, !(m-1-1>2), combined with the other predicates, forces m to be 4, and no other value. This also demonstrates, counter to the comment, that during proving, either m-1-1!=1 is derived, or the m-1-1=1 case is excluded, because m-1-1!=1 is not in the antecedent.

from hipsleek.

For the inductive case in #1 (comment), it seems evenness is important only when the array size is not a single variable.

This conclusion comes from: checkentail r::arr_seg<m> |- r::arr_seg<n>. being valid, checkentail r::arr_seg<m+m> |- r::arr_seg<n+n>. being invalid despite having the same form as the first entailment, and checkentail r::arr_seg<m+m> & m+m=n+n |- r::arr_seg<n+n>. is valid when m+m is known to be n+n, i.e. is known to be even. It should be noted that checkentail r::arr_seg<m+m> & m=n |- r::arr_seg<n+n>. is also valid.

Start of aside:
There was a hunch that implicit universal quantifiers are causing this behavior. However, upon careful analysis, it turns out the root cause was another issue. So feel free to skip this aside.
Thinking about how implicit universal quantifiers are represented in hipsleek: checkentail r::arr_seg<m+m> |- r::arr_seg<n+n>. is invalid because implicit universal quantifiers are introduced by the proof step:

x::node<a> |- x::node<b>
——————— 
\forall x,a,b . (x::node<a> & a=b |- x::node<b>)

but m+m=n+n is not true for all m, n. This motivates wrapping n in an existential on the consequent, so that the universal quantifier introduction is modified:

x::node<a> |- (exists b: x::node<b>)
—————————— 
\forall x,a (x::node<a> |- (exists b: x::node<b> & a=b)) 

and we can check that checkentail r::arr_seg<m+m> |- (exists n: r::arr_seg<n+n>). is valid.
End of aside.

Assuming array size is even, proving any array size is valid, witnessed by checkentail r::arr_seg<m+m> |- r::arr_seg<n>.. Assuming array size is even, proving array size is even is invalid, witnessed by checkentail r::arr_seg<m+m> |- r::arr_seg<n+n>..

We investigate further into why checkentail r::arr_seg<m+m> |- r::arr_seg<n+n>. is invalid. do_match fails with fc_message: (((2<=flted_24_126 & r!=null) | (flted_24_126=1 & r!=null))) & flted_24_126=m+m |- flted_24_126=n+n.. First, notice that checkentail (((flted_24_126=1 & r!=null))) & flted_24_126=m+m |- flted_24_126=n+n. is valid. So, we simplify the fc_message to checkentail 2<=flted_24_126 & flted_24_126=m+m |- flted_24_126=n+n..

We investigate further into why the inductive case in #1 (comment) is invalid, by running checkentail x::arr_seg<m> & m=2*n & n>1 & q=x+1 & r=q+1 & m>1 |- x::ch_star<Anon_18> * q::ch_star<Anon_19> * r::int_arr_seg<n-1>. and looking at the fc_message of do_match@9 of invocation ./sleek --pprint -dre="compute_actions\|do_match" file.slk, which is 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) |- exists(alpha:alpha+alpha=flted_6_172).. Note the similarity in form to checkentail 2<=flted_24_126 & flted_24_126=m+m |- flted_24_126=n+n..

So checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) |- (exists alpha:alpha+alpha=flted_6_172). is invalid, as expected. With the intuition from the start of this comment, that evenness is important, in mind, we non-exhaustively split up this entailment into 28 entailments with 28 instantiations of flted_6_172, from flted_6_172=1 to flted_6_172=28:

checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=1 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=2 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=3 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=4 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=5 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=6 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=7 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=8 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=9 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=10 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=11 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=12 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=13 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=14 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=15 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=16 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=17 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=18 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=19 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=20 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=21 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=22 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=23 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=24 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=25 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=26 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=27 |- (exists alpha:alpha+alpha=flted_6_172).
checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) & flted_6_172=28 |- (exists alpha:alpha+alpha=flted_6_172).

It turns out that all entailments with even values of flted_6_172 are valid, while all entailments with odd values of flted_6_172 are invalid. This is to be expected, since flted_6_172+1+1=n+n is one of the pure predicates in the antecedent, saying that flted_6_172 must be even. So, it is not the case that hipsleek cannot deduce that flted_6_172 is even from the pure predicate flted_6_172+1+1=n+n.

From this, we say that hipsleek cannot, given an entailment such that the entailment is valid with flted_6_172 ranging over even values and the entailment is valid with false context with flted_6_172 ranging over odd values, conclude that the entailment with flted_6_172 ranging over all values is valid.

from hipsleek.

Recall the fc_message in #1 (comment), as an invalid entailment: checkentail 1<n & 1<(n+n) & (1+x)!=x & (1+1+x)!=(1+x) & (1+1+x)!=x & x!=null & (1+x)!=null & flted_6_172+1+1=n+n & 1<(flted_6_172+1) & (((2<=flted_6_172 & (1+1+x)!=null) | (flted_6_172=1 & (1+1+x)!=null))) |- (exists alpha:alpha+alpha=flted_6_172)..

This is simplified to the invalid entailment checkentail 1<n & 2<=f & f+1+1=n+n |- (exists a:a+a=f).. On the other hand, checkentail 1<n & 2<=f & f=n+n |- (exists a:a+a=f). is valid. So, the prescence of 1+1 does something with hipsleek's ability to deduce that f is even. But this is unexpected, because hipsleek knows n>1, so n-1>=1, and f=n-1+n-1>=2, which is not contradictory.

Comparing the files logs/no_eps_proof_log_file_slk.txt output by ./sleek --en-logging-txt --pprint file.slk on checkentail 1<n & 2<=f & f=n+n |- (exists a:a+a=f). and checkentail 1<n & 2<=f & f+1+1=n+n |- (exists a:a+a=f). does not show why the second entailment fails, but the comparison does show at which call to the prover the two files diverge. For checkentail 1<n & 2<=f & f=n+n |- (exists a:a+a=f).:

 id: 126<4; prover: Z3; loc: file.slk_10:23_10:102; kind: Sleek_Entail(1)
 raw proof:no proof raw result:no result
 Imply: ante: 1<n & f=n+n & 2<=f
	     conseq:  exists(alpha_134:2*alpha_134=f)
 res: true

and for checkentail 1<n & 2<=f & f+1+1=n+n |- (exists a:a+a=f).:

 id: 126<4; prover: Z3; loc: file.slk_10:23_10:102; kind: Sleek_Entail(1)
 raw proof:no proof raw result:no result
 Imply: ante: 1<n & f+1+1=n+n & 2<=f
	     conseq:  exists(alpha_138:2*alpha_138=f)
 res: false

At commit 6c00b35, a diff between issues-1.slk.to_smt.fail_may and issues-1.slk.to_smt.valid shows, at to_smt@29 and to_smt@30, (assert (= (+ (+ 1 f) 1) (+ n n))) in issues-1.slk.to_smt.fail_may instead of (assert (= f (+ n n))) in issues-1.slk.to_smt.valid, and this huge chunk in issues-1.slk.to_smt.fail_may missing in issues-1.slk.to_smt.valid:

(====)
to_smt@31
to_smt inp1 :
to_smt@31 EXIT:;Variables declarations
(declare-fun f () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (exists ((alpha Int)) (= (+ alpha alpha) f)))
;Negation of Consequence
(assert (not false))
(check-sat)

(====)
to_smt@32
to_smt inp1 :
to_smt@32 EXIT:;Variables declarations
(declare-fun n () Int)
(declare-fun f () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (exists ((alpha Int)) (= (+ alpha alpha) f)))
;Negation of Consequence
(assert (not false))
(check-sat)

(====)
to_smt@33
to_smt inp1 :
to_smt@33 EXIT:;Variables declarations
(declare-fun n () Int)
(declare-fun f () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (+ alpha alpha) f))))
;Negation of Consequence
(assert (not false))
(check-sat)

Other differences include:

1. issues-1.slk.to_smt.29 and issues-1.slk.to_smt.32 differ only because (assert (exists ((alpha Int)) (= (+ alpha alpha) f))) exists only in issues-1.slk.to_smt.32.
2. issues-1.slk.to_smt.30 and issues-1.slk.to_smt.32 differ only because one asserts (exists ((alpha Int)) ...) and the other asserts (not (exists ((alpha Int)) ...)).
3. issues-1.slk.to_smt.30 and issues-1.slk.to_smt.33 differ not only because (assert (not (exists ((alpha Int)) (= (+ alpha alpha) f)))) exists only in issues-1.slk.to_smt.33, but also under ;Negation of Consequence, issues-1.slk.to_smt.30 has (assert (not (exists ((alpha_134 Int)) (= (* 2 alpha_134) f)))) while issues-1.slk.to_smt.33 has (assert (not false)). So, actually, issues-1.slk.to_smt.30 and issues-1.slk.to_smt.33 are equivalent.

Because function@calls of the form smt_imply@n do not always show for every to_smt@n function call, we verify the satisfiability of the following to_smt@n on https://rise4fun.com/z3:

1. to_smt@29: sat, because there is no contradictory assertion. From (assert (= (+ (+ 1 f) 1) (+ n n))) we know f is even, but nothing is asserted with the knowledge that f is even.
2. to_smt@31: sat, because there is no contradictory assertion. From (assert (exists ((alpha Int)) (= (+ alpha alpha) f))) we know f is even, but nothing is asserted with the knowledge that f is even.
3. to_smt@32: sat, because from (assert (= (+ (+ 1 f) 1) (+ n n))) we know f is even, and so (exists ((alpha Int)) (= (+ alpha alpha) f)).
4. to_smt@30: unsat, because (not (exists ((alpha_134 Int)) (= (* 2 alpha_134) f))) is false. See both above, on differences, point 2, as well as here, point 3.
5. to_smt@33: unsat, because (not (exists ((alpha Int)) (= (+ alpha alpha) f))) is false. See both above, on differences, point 3, as well as here, point 4 and point 3.

It was found that function@calls of the form smt_imply@n do not always show for every to_smt@n function call, because to_smt is also being called by the function is_sat. It was also found that to_smt is only called by these two functions. So, invoking ./sleek -dre="to_smt\|smt_imply\|is_sat\b" issues-1.slk at a3424c7, where \b denotes a word boundary, and is needed to prevent regex matching is_sat_tp among others, ensures all to_smt function calls have the form to_smt@m@n, that is, the call number @m belongs to to_smt, while the call number @n belongs to either some smt_imply or some is_sat.

A supposed disparity was found between smt_imply@35 and to_smt@36@35 on invoking ./sleek -dre="to_smt\|smt_imply" issues-1.slk at a3424c7. smt_imply@35 EXITs with true, but to_smt@36@35 has a SMT-LIB input which is unsat. This was double-confirmed by invoking ./sleek -dre="to_smt\|smt_imply\|is_sat\b\|Z3:check_formula" issues-1.slk at a3424c7, where smt_imply@131 EXITs with true, but Z3:check_formula@133@131 EXITs with unsat, and Z3:check_formula@133@131 has a SMT-LIB input which is identical to to_smt@132@131's.

However, this supposed disparity is actually expected, since smtsolver.ml:1134-1136 is:

      match output.sat_result with
      | Sat -> false
      | UnSat -> true

so smt_imply EXITs with true when check_formula EXITs with unsat.

from hipsleek.

Invoking ./sleek -dre="to_smt\|smt_imply\|is_sat\b\|Z3:check_formula" issues-1.slk at bbc5d44 (in contrast to at a3424c7 in comment #1 (comment)) shows smt_imply@131 EXITs with false, Z3:check_formula@133@131 EXITs with unknown, and Z3:check_formula@133@131 has a SMT-LIB input which is identical to to_smt@132@131's.

From https://stackoverflow.com/q/63191920, Z3 outputs unknown because weaker subsolvers are used when Z3 is run in "incremental mode". Whenever there are (push) or (pop) statements, Z3 is run in "incremental mode".

The solution is to stop Z3 from using weaker subsolvers, by using (reset) instead of (push) and (pop).

So, I tried two separate things:

1. Use (reset) whenever (push) or (pop) are used, everywhere. Set z3_sat_timeout_limit to 20.0. However, invoking ./sleek -dre="to_smt\|smt_imply\|is_sat\b\|Z3:check_formula" issues-1.slk at bbc5d44 with (reset) instead of (push) and (pop) leads to Z3:check_formula EXITing with nothing, and the entailment is still invalid:

   (====)
   to_smt@127@126
   to_smt inp1 :
   to_smt@127 EXIT:;Variables declarations
   (declare-fun n () Int)
   (declare-fun f () Int)
   ;Relations declarations
   ;Axioms assertions
   ;Antecedent
   (assert (< 1 n))
   (assert (<= 2 f))
   (assert (= f (+ n n)))
   (assert (not (exists ((alpha Int)) (= (+ alpha alpha) f))))
   ;Negation of Consequence
   (assert (not false))
   (check-sat)
   Nested Timer(timeout)
    Timeout after 20. secs
   [smtsolver.ml]Timeout when checking sat!20. Restarting z3 after ... 23 invocations. Stop z3... 23 invocations Starting z3...
   
   (====)
   Z3:check_formula@128@126
   Z3:check_formula inp1 :;Variables declarations
   (declare-fun n () Int)
   (declare-fun f () Int)
   ;Relations declarations
   ;Axioms assertions
   ;Antecedent
   (assert (< 1 n))
   (assert (<= 2 f))
   (assert (= f (+ n n)))
   (assert (not (exists ((alpha Int)) (= (+ alpha alpha) f))))
   ;Negation of Consequence
   (assert (not false))
   (check-sat)
   Z3:check_formula inp2 :20.
   Z3:check_formula@128 EXIT:
   
   (====)
   is_sat#1@126
   is_sat#1 inp1 : 1<n & 2<=f & f=n+n & !(exists(alpha:alpha+alpha=f))
   is_sat#1@126 EXIT:true
   
   (====)
   is_sat#1@129
   is_sat#1 inp1 : exists(alpha:alpha+alpha=f)
   is_sat#1@129 EXIT:true
   
   (====)
   is_sat#1@130
   is_sat#1 inp1 : 1<n & 2<=f & f=n+n & exists(alpha:alpha+alpha=f)
   is_sat#1@130 EXIT:true
   
   (====)
   is_sat#1@131
   is_sat#1 inp1 : 1<n & 2<=f & f=n+n & !(exists(alpha:alpha+alpha=f))
   is_sat#1@131 EXIT:true
   
   Entail 1: Fail.(may) cause: 1<n & 2<=f & f=n+n |-  exists(alpha:alpha+alpha=f). LOCS:[19;1] (may-bug)
   
   Residue:
   
     MaybeErr Context:
      fe_kind: MAY
      fe_name: logical bug
      fe_locs: {
        fc_message:  1<n & 2<=f & f=n+n |-  exists(alpha:alpha+alpha=f). LOCS:[19;1]I (may-bug)
        fc_current_lhs_flow: {FLOW,(20,21)=__norm#E}
      }
    [[empty]]
    CEX:false
   Validate 1: Expecting(3)Valid BUT got : Fail_May
   

   I suspect no timeout will be high enough, because I suspect Z3 is increasing the number of bits used to represent the even integer f without bound, because there will never be a f where two alphas do not make a f.
2. Use (reset) whenever (push) or (pop) are used, only when Z3's (check-sat) outputs a unknown.

At commit c937a7f, issues-1.slk.iget_answer.rec seems to show that thing 2 that was tried solves the issue (in contrast to issues-1.slk.iget_answer.unknown).

from hipsleek.

Fixed by 2e37560, with solution as stated in #1 (comment).

from hipsleek.

This comment documents solutions alternative to the solution in comment #1 (comment). That is, these solutions do not use (reset).

Sometimes, when quantifiers are involved, Z3's theories are incomplete, shown by a (get-info :reason-unknown) statement. Invoking z3 -smt2 on:

(push)
(declare-fun f () Int)
(declare-fun n () Int)
(assert (< 1 n))
(assert (<= 2 f))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (not (exists ((alpha Int)) (= (* 2 alpha) f))))
(check-sat)
(get-info :reason-unknown)
(pop)

outputs:

unknown
(:reason-unknown "(incomplete quantifiers)")

Observe that (assert (not (exists ((alpha Int)) (= (* 2 alpha) f)))) makes output unsat with (assert (= f (+ n n))) because Z3 can instantiate alpha=n, and similarly, (assert (not (exists ((alpha Int)) (= (* 2 alpha) (+ 2 f))))) makes output unsat with (assert (= (+ (+ 1 f) 1) (+ n n))) because Z3 can instantiate alpha=n.

However, (assert (not (exists ((alpha Int)) (= (* 2 alpha) f)))) makes output unknown with (assert (= (+ (+ 1 f) 1) (+ n n))) because Z3 cannot instantiate alpha=n-1, so has to brute-force the instantiation, leading to timeout.

Intuitively, Z3 instantiates the existential variable alpha to infinitely many concrete values n, without timing out, when the existential body matches a previous assertion. Intuitively, this is syntactic, and no brute-force enumeration is performed.

So, we have two choices to solve this:

1. Change the proposition in the consequent to (assert (not (exists ((alpha Int)) (= (* 2 alpha) (+ 2 f))))). This is equivalent to performing checkentail 1<n & 2<=f & f+1+1=n+n |- (exists a:a+a=f+1+1)..
2. Change the proposition in the antecedent to (assert (forall ((n Int)) (= f (+ n n)))) instead (note: changing the proposition to (assert (forall ((n Int)) (= (+ (+ 1 f) 1) (+ n n)))) works too). This is equivalent to performing checkentail 1<n & 2<=f & (forall n:f+1+1=n+n) |- (exists a:a+a=f)..

Choice 2 is impossible, because sleek does not syntactically allow (forall n:...) in the antecedent. As @chinwn pointed out, the predicate Univ(n) can be used in the antecedent to have the semantics that n is universally quantified in sleek. But there are two problems with this:

1. sleek's checkentail Univ(n) |- true. should be translated to SMT-LIB (forall ((n Int)) ...) , but this does not happen:

   (declare-fun n () Int)
   ;Relations declarations
   (declare-fun Univ (Int) Bool)
   ;Axioms assertions
   ;Antecedent
   (assert (Univ n))
   ;Negation of Consequence
   (assert (not false))
   (check-sat)
   

2. Unlike forall, Univ(n) does not encode any proposition for n to range over. This means the translator must search over the entire entailment for which propositions involve n, and then construct the SMT-LIB input (forall ((n Int)) (...)) that encapsulates all these propositions. This is added code complexity.

So choice 1 seems the way to go, but checkentail 1<n & 2<=f & f+1+1=n+n |- (exists a:a+a=f+1+1). results in fc_message: 1<n & 2<=f & 1+f+1=n+n |- exists(alpha:alpha+alpha=f). Notice the lack of f+1+1 in the body of the existential. I believe this is a bug in hipsleek.

from hipsleek.

Reopening due unexpected list of ./sleek testcases/ex5c.slk at 9d5576d with a >= 0 & b >= 0 not in lemmas splitint and splitchar, [24,25,26,29,30,31,33,34,35,37,38,40,41,42,43,44,45,47,48,49,50,51,53], not being different than the first row of #1 (comment) (that is, [24,25,26,29,30,31,33,34,35,37,38,40,41,42,43,44,45,47,48,49,50,51,53]).

Also, the investigations of entailment 32 that started at #1 (comment) is not complete, because ./sleek --pnum 32 testcases/ex5c.slk still gives unexpected at 9d5576d.

from hipsleek.

Continuing investigations of entailment 32 that started at #1 (comment), there are two important differences I want to highlight at do_match@5:

1. testcases/ex5c.slk.geqno.subst:237: a_315=4*flted_307_304
2. testcases/ex5c.slk.geq:244: es_pure: flted_16_310=4*flted_307_304

where es_pure is the residual pure formula on the RHS of the entailment. This means *.geqno.subst is able to derive that a_315=flted_16_310 through do_match@5, but *.geq is not able to.

In #1 (comment), at commit 9d6ecf4, the one important difference I want to highlight at @5!:0: 0: **solver.ml#9386:heap_entail_empty_heap: folding: res_ctx: is:

1. testcases/ex5c.slk.trace-log-num_5.geq:1979: es_pure: flted_16_310=4*flted_307_304

Looking at solver.ml, res_ctx is given by let res_ctx = Ctx (CF.add_to_estate res_es "folding performed") in and let res_ctx = elim_unsat_ctx prog (ref 1) res_ctx in.

Another important difference is:

1. testcases/ex5c.slk.trace-log-num_5.geq:1158: flted_16_310=4*flted_307_304

where this conseq1 must come from conseq in let ctx, proof = heap_entail_empty_rhs_heap_one_flow prog conseq is_folding estate_orig1 lhs1 rhs_p rhs_matched_set pos in (i.e. from the first code block below), because the only two code blocks that contain calls to heap_entail_empty_rhs_heap_one_flow also respectively contain these lines:

1. let () = x_tinfo_hp (add_str "TODO : not set classic_flag" string_of_bool) classic_flag no_pos in prints @5! **solver.ml#8653:TODO : not set classic_flag:false.
2. let () = x_tinfo_pp "first if-then" no_pos in does not print anything.

So the first occurence of conseq at the call in the first code block is the input argument to heap_entail_empty_rhs_heap_x.

Another important difference is:

1. testcases/ex5c.slk.trace-log-num_5.geq:434: flted_16_310=4*flted_307_304

which is printed by let () = x_dinfo_hp (add_str "tmp_conseq" (Cprinter.string_of_formula)) tmp_conseq pos in. Tracing tmp_conseq and new_conseq_p:

1. solver.ml:11234: let tmp_conseq = mkBase r_h new_conseq_p r_vp r_t r_fl r_a pos in
2. solver.ml:11221: let new_conseq_p,new_ante_p =
3. solver.ml:11149: let new_conseq_p = (MCP.memoise_add_pure_N new_conseq_p p_conseq) in

However, it is known that the same @5!:0: 0: **solver.ml#11159:pure_new_conseq_p: flted_16_310=4*flted_307_304 is printed in both testcases/ex5c.slk.trace-log-num_5.geq and testcases/ex5c.slk.trace-log-num_5.geqno.subst, from the code let () = y_dinfo_hp (add_str "pure_new_conseq_p" !CP.print_formula) pure_new_conseq_p in .

Debugging new_conseq_p in c8edd23, the first three prints of pure_conseq_p in testcases/ex5c.slk.trace-log-num_5.debug.geq and testcases/ex5c.slk.trace-log-num_5.debug.geqno are identical up to renaming, but the fourth print is different: testcases/ex5c.slk.trace-log-num_5.debug.geq prints @5!:0: 0: **solver.ml#11229:pure_new_conseq_p: flted_16_310=4*flted_307_304 while testcases/ex5c.slk.trace-log-num_5.debug.geqno prints @5!:0: 0: **solver.ml#11229:pure_new_conseq_p: true. So this code block in solver.ml must be the culprit:

          let new_conseq_p,new_ante_p =
            if conseq_lst_univ!=[] then
              let conseq_univ = CP.join_conjunctions conseq_lst_univ in
              let (flag,ante) = process_early univ_vs new_ante_p conseq_univ in
              if flag then (new_conseq_p2,ante)
              else (new_conseq_p,new_ante_p)
            else new_conseq_p,new_ante_p in

From 5d582eb , the print of pure_conseq_p in testcases/ex5c.slk.trace-log-num_5.debug.geq is @5!:0: 0: **solver.ml#11229:pure_new_conseq_p: flted_16_310=4*flted_307_304, while testcases/ex5c.slk.trace-log-num_5.debug.geqno is @5!:0: 0: **solver.ml#11226:pure_new_conseq_p2: true. This means flag given by let (flag,ante) = process_early univ_vs new_ante_p conseq_univ in is true in one and false in another. Tracing flag:

1. solver.ml:11213-11217:

            if b then
              let r = TP.univ_rhs_store # get_rm in
              let new_ante = CP.mkAnd lhs1 r no_pos in
              (b,MCP.mix_of_pure new_ante)
            else (b,new_ante_p)
   

2. tpdispatcher.ml:3746:3750:

    let (b,_,_) as r = x_add imply_timeout ante0 new_conseq imp_no timeout process in
    let () = y_dinfo_hp (add_str "imply_timeout_univ: b " string_of_bool) b in
    if b then
      let () = univ_rhs_store # set conseq0 in r
    else r
   

and we see the print of imply_timeout_univ in testcases/ex5c.slk.trace-log-num_5.debug.geq is @5!:0: 0: **tpdispatcher.ml#3747:imply_timeout_univ: b :false, while testcases/ex5c.slk.trace-log-num_5.debug.geqno is @5!:0: 0: **tpdispatcher.ml#3747:imply_timeout_univ: b :true.

Also, the result from the SMT solver is printed in testcases/ex5c.slk.trace-log-num_5.debug.geq as @5!:0: 0: **tpdispatcher.ml#3583:res: :false while testcases/ex5c.slk.trace-log-num_5.debug.geqno is @5!:0: 0: **tpdispatcher.ml#3583:res: :true.

At 6fcc70a, although the Z3:check_formula function calls called by compute_actions@49 in testcases/ex5c.slk.trace-log-num_54.debug.geqno and compute_actions@50 in testcases/ex5c.slk.trace-log-num_55.debug.geq are mostly similar, testcases/ex5c.slk.trace-log-num_54.debug.geqno has four Z3:check_formula function calls, while testcases/ex5c.slk.trace-log-num_55.debug.geq has five. The extra Z3:check_formula@49 in testcases/ex5c.slk.trace-log-num_55.debug.geq is printed as:

(====)
Z3:check_formula@49
Z3:check_formula inp1 :;Variables declarations
(declare-fun flted_306_285 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (= flted_306_285 5))
(assert (<= 2 flted_306_285))
;Negation of Consequence
(assert (not (<= 0 flted_306_285)))
(check-sat)
Z3:check_formula inp2 :10.
Z3:check_formula@49 EXIT:unsat

Another difference in Z3:check_formula function@calls is between @55!:0: 0: **smtsolver.ml#230:NONE # and the @5!:0: 0: **tpdispatcher.ml#3583:res: from before, with testcases/ex5c.slk.trace-log-num_54.debug.geqno having:

(====)
Z3:check_formula@55@54
Z3:check_formula inp1 :;Variables declarations
(declare-fun b_306 () Int)
(declare-fun a_307 () Int)
(declare-fun q_308 () Int)
(declare-fun flted_306_277 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (= flted_306_277 (+ b_306 a_307)))
(assert (= (+ a_307 x) q_308))
(assert (= flted_306_277 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (= flted_306_277 5) (= y (+ x 4)))))
(check-sat)
Z3:check_formula inp2 :0.
Z3:check_formula@55 EXIT:unsat

and testcases/ex5c.slk.trace-log-num_55.debug.geq having:

(====)
Z3:check_formula@56@55
Z3:check_formula inp1 :;Variables declarations
(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 0 b_316))
(assert (<= 0 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (and (and (= y (+ x 4)) (= flted_306_285 5)) (<= 0 flted_307_304)) (<= flted_307_304 1))))
(check-sat)
Z3:check_formula inp2 :0.
Z3:check_formula@56 EXIT:sat

It turns out that removing (and (<= 0 flted_307_304)) (<= flted_307_304 1)) from the consequent in Z3:check_formula@56@55 from testcases/ex5c.slk.trace-log-num_55.debug.geq makes (check-sat) output unsat. That is, z3 -smt file where file is:

;Variables declarations
(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 0 b_316))
(assert (<= 0 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (= y (+ x 4)) (= flted_306_285 5))))
(check-sat)

outputs unsat.

Also, adding (assert (<= 0 flted_307_304)) and (assert (<= flted_307_304 1)) into the antecedent in Z3:check_formula@56@55 from testcases/ex5c.slk.trace-log-num_55.debug.geq makes (check-sat) output unsat. That is, z3 -smt2 file where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
(assert (<= 0 flted_307_304))
(assert (<= flted_307_304 1))
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 0 b_316))
(assert (<= 0 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (and (and (= y (+ x 4)) (= flted_306_285 5)) (<= 0 flted_307_304)) (<= flted_307_304 1))))
(check-sat)

outputs unsat.

So the input to Z3 is bad. This input is the output of omega. Keeping this in mind, note that the previous comment
#1 (comment) already listed an important difference between inputs to omega:

1. testcases/ex5c.slk.trace-log-num_5.geq:392-395 has

   @5! **omega.ml#901:simplify_ops_x(after trans_arr)::
    exists(b_316:0<=b_316 & flted_306_285=5 & y=4+x & 
                 flted_306_285=b_316+(4*flted_307_304) & 0<=(4*flted_307_304))
   @5! **omega.ml#454:omega inp:{[y, x, flted_306_285, flted_307_304] : ( (exists (b_316:((((0 <= b_316) & (flted_306_285 = 5)) & (y = 4 + x)) & ((flted_306_285 = b_316 + 4(flted_307_304)) & (0 <= 4(flted_307_304)))))) )};
   

   whereas testcases/ex5c.slk.trace-log-num_5.geqno.subst:393-397 has

   @5! **omega.ml#901:simplify_ops_x(after trans_arr)::
    exists(q_314:flted_306_285=5 & y=4+x & 
                 exists(b_316:flted_306_285=b_316+(4*flted_307_304) & 
                              (4*flted_307_304)+x=q_314))
   @5! **omega.ml#454:omega inp:{[y, flted_306_285, flted_307_304, x] : ( (exists (q_314:(((flted_306_285 = 5) & (y = 4 + x)) &  (exists (b_316:((flted_306_285 = b_316 + 4(flted_307_304)) & (4(flted_307_304) + x = q_314)))) ))) )};
   

So here, we continue listing the important differences between testcases/ex5c.slk.trace-log-num_5.geq and testcases/ex5c.slk.trace-log-num_5.geqno.subst at commit 9d6ecf4.

1. testcases/ex5c.slk.trace-log-num_5.geq:401-414 has

   @5!:0: 0: **tpdispatcher.ml#3548:ante 1: : flted_306_285=b_316+a_315 & a_315+x=q_314 & 0<=a_315 & 0<=b_316 & 
    flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3554:ante 3: : flted_306_285=b_316+a_315 & a_315+x=q_314 & 0<=a_315 & 0<=b_316 & 
    flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3556:ante 4: : flted_306_285=b_316+a_315 & a_315+x=q_314 & 0<=a_315 & 0<=b_316 & 
    flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3341:IMP #211
   @5!:0: 0: **tpdispatcher.ml#3342:imply_timeout: ante:  0<=b_316 & 0<=a_315 & flted_306_285=b_316+a_315 & a_315+x=q_314 & 
    flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3343:imply_timeout: conseq:  y=x+4 & flted_306_285=5 & 0<=flted_307_304 & flted_307_304<=1
   @5! **tpdispatcher.ml#1424:Ann Vars:[]
   @5! **tpdispatcher.ml#1425:Inv: 0<=b_316 & 0<=a_315 & flted_306_285=b_316+a_315 & a_315+x=q_314 & 
    flted_306_285=5 & y=4+x
   

   testcases/ex5c.slk.trace-log-num_5.geqno.subst:403-414 has

   @5!:0: 0: **tpdispatcher.ml#3548:ante 1: : flted_306_285=b_316+a_315 & a_315+x=q_314 & flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3554:ante 3: : flted_306_285=b_316+a_315 & a_315+x=q_314 &
   flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3556:ante 4: : flted_306_285=b_316+a_315 & a_315+x=q_314 &
   flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3341:IMP #210
   @5!:0: 0: **tpdispatcher.ml#3342:imply_timeout: ante:  flted_306_285=b_316+a_315 & a_315+x=q_314 & 
   flted_306_285=5 & y=4+x
   @5!:0: 0: **tpdispatcher.ml#3343:imply_timeout: conseq:  flted_306_285=5 & y=x+4
   @5! **tpdispatcher.ml#1424:Ann Vars:[]
   @5! **tpdispatcher.ml#1425:Inv: flted_306_285=b_316+a_315 & a_315+x=q_314 &
    flted_306_285=5 & y=4+x
   

2. testcases/ex5c.slk.trace-log-num_5.geq:392-400 has

   @5! **omega.ml#901:simplify_ops_x(after trans_arr)::
    exists(b_316:0<=b_316 & flted_306_285=5 & y=4+x & 
                 flted_306_285=b_316+(4*flted_307_304) & 0<=(4*flted_307_304))
   @5! **omega.ml#454:omega inp:{[y, x, flted_306_285, flted_307_304] : ( (exists (b_316:((((0 <= b_316) & (flted_306_285 = 5)) & (y = 4 + x)) & ((flted_306_285 = b_316 + 4(flted_307_304)) & (0 <= 4(flted_307_304)))))) )};
   
   @5! **omega.ml#461:omega out:{[y,y-4,5,flted_307_304]: 0 <= flted_307_304 <= 1}
   @5! **omega.ml#454:omega inp:pairwisecheck {[x, y, flted_306_285, flted_307_304] : (((((x + 4 = y) & (flted_306_285 = 5)) & (0 <= flted_307_304)) & (flted_307_304 <= 1)))};
   
   @5! **omega.ml#461:omega out:{[x,x+4,5,flted_307_304]: 0 <= flted_307_304 <= 1}
   

   whereas testcases/ex5c.slk.trace-log-num_5.geqno.subst:393-402 has

   @5! **omega.ml#901:simplify_ops_x(after trans_arr)::
    exists(q_314:flted_306_285=5 & y=4+x & 
                 exists(b_316:flted_306_285=b_316+(4*flted_307_304) & 
                              (4*flted_307_304)+x=q_314))
   @5! **omega.ml#454:omega inp:{[y, flted_306_285, flted_307_304, x] : ( (exists (q_314:(((flted_306_285 = 5) & (y = 4 + x)) &  (exists (b_316:((flted_306_285 = b_316 + 4(flted_307_304)) & (4(flted_307_304) + x = q_314)))) ))) )};
   
   @5! **omega.ml#461:omega out:{[y,5,flted_307_304,y-4]}
   @5! **omega.ml#454:omega inp:pairwisecheck {[flted_306_285, x, y] : (((flted_306_285 = 5) & (x + 4 = y)))};
   
   @5! **omega.ml#461:omega out:{[5,x,x+4]}
   

Notably:

1. @5! **omega.ml#901:simplify_ops_x(after trans_arr)::: testcases/ex5c.slk.trace-log-num_5.geq:393-394 has 0<=b_316 and 0<=(4*flted_307_304), while testcases/ex5c.slk.trace-log-num_5.geqno.subst:396 has (4*flted_307_304)+x=q_314.
2. @5! **omega.ml#454:omega inp:: testcases/ex5c.slk.trace-log-num_5.geq:395 has 0<=b_316 and 0 <= 4(flted_307_304), while testcases/ex5c.slk.trace-log-num_5.geqno.subst:397 has 4(flted_307_304) + x = q_314.
3. @5! **omega.ml#461:omega out:: testcases/ex5c.slk.trace-log-num_5.geq:397 has 0 <= flted_307_304 <= 1, while testcases/ex5c.slk.trace-log-num_5.geqno.subst:399 does not have it.
4. @5! **omega.ml#454:omega inp:: testcases/ex5c.slk.trace-log-num_5.geq:398 has 0 <= flted_307_304 and flted_307_304 <= 1, while testcases/ex5c.slk.trace-log-num_5.geqno.subst:400 does not have them.
5. @5! **omega.ml#461:omega out:: testcases/ex5c.slk.trace-log-num_5.geq:400 has 0 <= flted_307_304 <= 1, while testcases/ex5c.slk.trace-log-num_5.geqno.subst:402 does not have it.

For the entire block of @5!:0: 0: **tpdispatcher.ml prints, the only significant difference is testcases/ex5c.slk.trace-log-num_5.geq:410 has 0<=flted_307_304 & flted_307_304<=1 while testcases/ex5c.slk.trace-log-num_5.geqno.subst:411 does not. The other insignificant differences are that the formulas 0<=a_315 & 0<=b_316 are in testcases/ex5c.slk.trace-log-num_5.geq:401-414 but not testcases/ex5c.slk.trace-log-num_5.geqno.subst:403-414.

So the culprit here should be the inputs to omega, because the outputs of omega is given at:

1. testcases/ex5c.slk.trace-log-num_5.geq:397 as 0 <= flted_307_304 <= 1, which corresponds exactly to the output of ./oc file where file is:

   {[y, x, flted_306_285, flted_307_304] : ( (exists (b_316:((((0 <= b_316) & (flted_306_285 = 5)) & (y = 4 + x)) & ((flted_306_285 = b_316 + 4(flted_307_304)) & (0 <= 4(flted_307_304)))))) )};
   

2. testcases/ex5c.slk.trace-log-num_5.geq:400 as 0 <= flted_307_304 <= 1, which corresponds exactly to the output of ./oc file where file is:

   pairwisecheck {[x, y, flted_306_285, flted_307_304] : (((((x + 4 = y) & (flted_306_285 = 5)) & (0 <= flted_307_304)) & (flted_307_304 <= 1)))};
   

This output makes sense, because assuming all variables are integers, and we have at testcases/ex5c.slk.trace-log-num_5.geq:395 the constraints flted_306_285 = b_316 + 4(flted_307_304), flted_306_285 = 5, 0 <= b_316 and 0 <= 4(flted_307_304), then there can only be two solutions to this set of constraints: either b_316=5 and flted_307_304=0 or b_316=1 and flted_307_304=1 (actually, the solution b_316=5 and flted_307_304=0 is rejected, because the invariant inv n>=1 in the definition of pred int_arr_seg<n> prohibits flted_307_304=0). In contrast, testcases/ex5c.slk.trace-log-num_5.geqno.subst:397 has only the constraints flted_306_285 = b_316 + 4(flted_307_304) and flted_306_285 = 5, where both b_316 and flted_307_304 range over the negative and positive integers, so there are infinitely many solutions to this set of constraints. So the guess at #1 (comment) was in the right direction.

This is a "semantic" bug. Both variables b_316 and flted_307_304 represent array sizes. Array sizes are never negative, that is, have a maximum range of 0 to infinity. So, it does not make sense that adding nonnegativity constraints makes the entailment invalid.

It is possible to derive flted_307_304 = 1, from which z3 -smt2 file outputs unsat where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
(assert (= flted_307_304 1))
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 0 b_316))
(assert (<= 0 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (and (and (= y (+ x 4)) (= flted_306_285 5)) (<= 0 flted_307_304)) (<= flted_307_304 1))))
(check-sat)

and from which ./oc file outputs {[y,y-4,5,1]} where file is:

{[y, x, flted_306_285, flted_307_304] : ( (exists (b_316:((((0 <= b_316) & (flted_306_285 = 5)) & (y = 4 + x)) & (((flted_306_285 = b_316 + 4(flted_307_304)) & (0 <= 4(flted_307_304))) & (1 = flted_307_304))))) )};

and from which ./oc file outputs {[x,x+4,5,1]} where file is:

pairwisecheck {[x, y, flted_306_285, flted_307_304] : ((((((x + 4 = y) & (flted_306_285 = 5)) & (0 <= flted_307_304)) & (flted_307_304 <= 1)) & (flted_307_304 = 1)))};

Let us see how to derive flted_307_304 = 1. Firstly, we derive flted_307_304 >= 1 from int_arr_seg<flted_307_304> and the invariant inv n>=1 in the definition of pred int_arr_seg<n>. Secondly, we derive b_316 >= 0 from a>=0 & b>=0 in lemma "splitchar" self::arr_seg<a+b>. Thirdly, any flted_307_304>=2 violates the constraints flted_306_285 = 5, b_316 >= 0 and flted_306_285 = b_316 + 4(flted_307_304). So we conclude that flted_307_304 = 1.

from hipsleek.

Comment #1 (comment) is wrong in saying flted_307_304 = 1 is derivable.

The comment claims that flted_307_304 >= 1 is derived from int_arr_seg<flted_307_304> and the invariant inv n>=1 in the definition of pred int_arr_seg<n>. However, the heap predicate int_arr_seg<flted_307_304> is on the RHS of the entailment. So, flted_307_304 >= 1 is not derived. Rather, flted_307_304 >= 1 remains to be proved.

Similarly, the comment claims that the solution b_316=5 and flted_307_304=0 is rejected, because the invariant inv n>=1 in the definition of pred int_arr_seg<n> prohibits flted_307_304=0. Again, the heap predicate int_arr_seg<flted_307_304> is on the RHS of the entailment. So, flted_307_304 >= 1 is not derived. Rather, flted_307_304 >= 1 remains to be proved.

So, the outputs of omega being 0 <= flted_307_304 <= 1 is completely correct.

As a reminder, the outputs of omega is given at:

1. testcases/ex5c.slk.trace-log-num_5.geq:397 as 0 <= flted_307_304 <= 1, which corresponds exactly to the output of ./oc file where file is:

   {[y, x, flted_306_285, flted_307_304] : ( (exists (b_316:((((0 <= b_316) & (flted_306_285 = 5)) & (y = 4 + x)) & ((flted_306_285 = b_316 + 4(flted_307_304)) & (0 <= 4(flted_307_304)))))) )};
   

2. testcases/ex5c.slk.trace-log-num_5.geq:400 as 0 <= flted_307_304 <= 1, which corresponds exactly to the output of ./oc file where file is:

   pairwisecheck {[x, y, flted_306_285, flted_307_304] : (((((x + 4 = y) & (flted_306_285 = 5)) & (0 <= flted_307_304)) & (flted_307_304 <= 1)))};
   

from hipsleek.

Continuing investigations with debug files at 6fcc70a, it is possible to derive a_315=4*flted_307_304, from which z3 -smt2 file outputs unsat where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (= a_315 (* 4 flted_307_304)))
(assert (<= 0 b_316))
(assert (<= 0 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (and (and (= y (+ x 4)) (= flted_306_285 5)) (<= 0 flted_307_304)) (<= flted_307_304 1))))
(check-sat)

Indeed, do_match@5 fails because the information a_315=4*flted_307_304 has been derived by hipsleek, but has been deleted. Indeed, comparing testcases/ex5c.slk.trace-log-num_5.geq:382-385:

@5!:0: 0: **tpdispatcher.ml#3745:new_conseq: exists(b_316:exists(a_315:exists(q_314:flted_306_285=b_316+a_315 & 
                                        a_315+x=q_314 & 0<=a_315 & 
                                        0<=b_316 & flted_306_285=5 & y=
                                        4+x & a_315=4*flted_307_304)))

with testcases/ex5c.slk.trace-log-num_5.geq:392-394:

@5! **omega.ml#901:simplify_ops_x(after trans_arr)::
 exists(b_316:0<=b_316 & flted_306_285=5 & y=4+x & 
              flted_306_285=b_316+(4*flted_307_304) & 0<=(4*flted_307_304))

shows that a_315=4*flted_307_304 has been discarded. A similar thing happens in testcases/ex5c.slk.trace-log-num_5.geqno.subst, but there, a_315=4*flted_307_304 is not crucial to entailment validity.

As hinted by the printout, omega.ml#901:simplify_ops_x prints the output of let pe = Trans_arr.translate_array_one_formula pe in. However, disabling array translation by adding the --dis-array-translate-out flag to ./sleek --dis-array-translate-out -dre="compute_actions\|do_match" --pnum 32 --trace-log-num 5 testcases/ex5c.slk did not change anything. So the cause of deletion must have occured earlier.

The immediate earlier occurence of pe is at the input of simplify_ops. However, looking at the source code of simplify, we know pe was not modified earlier. So, could continue debugging by backtracking to @5!:0: 0: **tpdispatcher.ml#3745 in testcases/ex5c.slk.trace-log-num_5.geq:382, and looking at tpdispatcher.ml:3745. However, testcases/ex5c.slk.trace-log-num.omega.geq:839 at 05fd67f shows (==smtsolver.ml#1281==), so we continue debugging at smtsolver.ml:1281 instead, where we discover that that call is debugged at smtsolver.ml:1293 with code Debug.no_1 "simplify" pr pr simplify pe.

So, we look at testcases/ex5c.slk.trace-log-num.simplify.geq at f0c1d05 (interestingly, Omega.simplify does not appear anywhere in testcases/ex5c.slk.trace-log-num.simplify.geq). At testcases/ex5c.slk.trace-log-num.simplify.geq:3490 at simplify(TP)@552@551, there is a_315=4*flted_307_304, but at testcases/ex5c.slk.trace-log-num.simplify.geq:3484 at simplify##@553@552@551, there is no a_315=4*flted_307_304. Furthermore, call @552 only calls @553.

So, we search the entire codebase for the string simplify(TP), and the only result is tpdispatcher.ml:2589. So we look at tpdispatcher.ml:2589, which is Debug.no_1 "simplify(TP)" pf pf simplify f, which calls simplify at tpdispatcher.ml:2580, which is:

let simplify (f:CP.formula): CP.formula = 
  x_add CP.elim_exists_with_simpl simplify f

So, we look at testcases/ex5c.slk.trace-log-num.elim_exists_with_simpl.geq at 54e5c44, which has:

(==tpdispatcher.ml#2581==)
elim_exists_with_simpl@580@579@578
elim_exists_with_simpl inp1 : exists(b_316:exists(a_315:exists(q_314:flted_306_285=b_316+a_315 & 
                                        a_315+x=q_314 & 0<=a_315 & 
                                        0<=b_316 & flted_306_285=5 & y=
                                        4+x & a_315=4*flted_307_304)))
elim_exists_with_simpl@580 EXIT: y=x+4 & flted_306_285=5 & 0<=flted_307_304 & flted_307_304<=1

To find out whether elim_exists_with_simpl is the culprit, simplify at tpdispatcher.ml:2580 was modified to be the identity function, so that testcases/ex5c.slk.trace-log-num.elim_exists_with_simpl.id.geq:3085-3094 is:

(====)
simplify(TP)@453@452
simplify(TP) inp1 : exists(b_332:exists(a_331:exists(q_330:flted_306_301=b_332+a_331 & 
                                        a_331+x=q_330 & 0<=a_331 & 
                                        0<=b_332 & flted_306_301=5 & y=
                                        4+x & a_331=4*flted_307_320)))
simplify(TP)@453 EXIT: exists(b_332:exists(a_331:exists(q_330:flted_306_301=b_332+a_331 & 
                                        a_331+x=q_330 & 0<=a_331 & 
                                        0<=b_332 & flted_306_301=5 & y=
                                        4+x & a_331=4*flted_307_320)))

However, a_331=4*flted_307_320 is still deleted somewhere at testcases/ex5c.slk.trace-log-num.elim_exists_with_simpl.id.geq:3102-3148:

@452!:0: 0: **tpdispatcher.ml#3549:ante 1: : flted_306_301=b_332+a_331 & a_331+x=q_330 & 0<=a_331 & 0<=b_332 & 
 flted_306_301=5 & y=4+x
@452!:0: 0: **tpdispatcher.ml#3555:ante 3: : flted_306_301=b_332+a_331 & a_331+x=q_330 & 0<=a_331 & 0<=b_332 & 
 flted_306_301=5 & y=4+x
@452!:0: 0: **tpdispatcher.ml#3557:ante 4: : flted_306_301=b_332+a_331 & a_331+x=q_330 & 0<=a_331 & 0<=b_332 & 
 flted_306_301=5 & y=4+x
@452!:0: 0: **tpdispatcher.ml#3342:IMP #159
@452!:0: 0: **tpdispatcher.ml#3343:imply_timeout: ante:  0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
 flted_306_301=5 & y=4+x
@452!:0: 0: **tpdispatcher.ml#3344:imply_timeout: conseq:  exists(b_337:0<=b_337 & flted_306_301=5 & y=4+x & 
              flted_306_301=b_337+(4*flted_307_320) & 0<=(4*flted_307_320))
(====)
simplify_imm_min_max@454@452
simplify_imm_min_max inp1 : (exists(b_337:0<=b_337 & flted_306_301=5 & y=4+x & 
               flted_306_301=b_337+(4*flted_307_320) & 0<=(4*flted_307_320)) | 
  !((0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
     flted_306_301=5 & y=4+x)))
simplify_imm_min_max@454 EXIT: (exists(b_337:0<=b_337 & flted_306_301=5 & y=4+x & 
               flted_306_301=b_337+(4*flted_307_320) & 0<=(4*flted_307_320)) | 
  !((0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
     flted_306_301=5 & y=4+x)))

(==tpdispatcher.ml#1787==)
simplify-syn@455@452
simplify-syn inp1 : (exists(b_337:0<=b_337 & flted_306_301=5 & y=4+x & 
               flted_306_301=b_337+(4*flted_307_320) & 0<=(4*flted_307_320)) | 
  !((0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
     flted_306_301=5 & y=4+x)))
simplify-syn@455 EXIT: (exists(v0:0<=v0 & v1=5 & v2=4+v3 & v1=v0+(4*v4) & 0<=(4*v4)) | 
  !((0<=v5 & 0<=v6 & v1=v5+v6 & v6+v3=v7 & v1=5 & v2=4+v3)))

@452! **tpdispatcher.ml#1424:Ann Vars:[]
@452! **tpdispatcher.ml#1425:Inv: 0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
 flted_306_301=5 & y=4+x
(====)
simplify_imm_min_max@456@452
simplify_imm_min_max inp1 : 0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
 flted_306_301=5 & y=4+x
simplify_imm_min_max@456 EXIT: 0<=b_332 & 0<=a_331 & flted_306_301=b_332+a_331 & a_331+x=q_330 & 
 flted_306_301=5 & y=4+x

(====)
simplify_imm_min_max@457@452
simplify_imm_min_max inp1 : exists(b_337:0<=b_337 & flted_306_301=5 & y=4+x & 
              flted_306_301=b_337+(4*flted_307_320) & 0<=(4*flted_307_320))
simplify_imm_min_max@457 EXIT: exists(b_337:0<=b_337 & flted_306_301=5 & y=4+x & 
              flted_306_301=b_337+(4*flted_307_320) & 0<=(4*flted_307_320))

From the following output, we know that imply_timeout_helper somewhere at tpdispatcher.ml:3549 has a bad ante input:

@452!:0: 0: **tpdispatcher.ml#3549:ante 1: : flted_306_301=b_332+a_331 & a_331+x=q_330 & 0<=a_331 & 0<=b_332 & 
 flted_306_301=5 & y=4+x

So we look at tpdispatcher.ml:3746 to find an eventual call to imply_timeout_helper. The call chain is: imply_timeout at tpdispatcher.ml:3746 -> imply_timeout at tpdispatcher.ml:3673 -> imply_timeout_helper at tpdispatcher.ml:3649-3654, which is:

          if (CP.rhs_needs_or_split conseq)&& not (no_andl ante) && !label_split_conseq then
            let conseq_disj = CP.split_disjunctions conseq in
            List.fold_left (fun (r1,r2,r3) d -> 
                if not r1 then x_add imply_timeout_helper ante d process ante_inner conseq_inner imp_no timeout
                else (r1,r2,r3) ) (false,[],None) conseq_disj 
          else imply_timeout_helper ante conseq process ante_inner conseq_inner imp_no timeout

where ante is:

        let ante = if CP.should_simplify ante0 then simplify_a 13 ante0 else ante0 in

which leads to:

let simplify_a (s:int) (f:CP.formula): CP.formula = 
  let pf = Cprinter.string_of_pure_formula in
  Debug.no_1_num s ("TP.simplify_a") pf pf simplify f

and back to:

let simplify (f : CP.formula) : CP.formula =
  let pf = Cprinter.string_of_pure_formula in
  Debug.no_1 "simplify(TP)" pf pf simplify f

but simplify was made to be the identity function, so the deletion of a_331=4*flted_307_320 must have occured earlier, in imply_timeout or before. Since there is no modification to ante0 in imply_timeout, the input to imply_timeout must have been bad, which is given at imply_timeout_univ at tpdispatcher.ml:3747.

At this point, looking at @5!:0: 0: **tpdispatcher.ml#3735:conseq0: a_315=4*flted_307_304 at testcases/ex5c.slk.trace-log-num_5.geq:376, I realized that neither ante0 nor ante are bad inputs. a_315=4*flted_307_304 is missing from the antecedent, simply because it is the consequent, and remains to be proven. So, of course a_315=4*flted_307_304 cannot be in the antecedent of the Z3 proof at the start of the comment. So this entire comment is void.

From #1 (comment), we know why the Z3 proof fails. However, we have yet to find a suitable modification to the antecedent in the Z3 proof to make it valid. This comment tried to find one ((assert (= a_315 (* 4 flted_307_304)))), but this is begging the question.

from hipsleek.

Although #1 (comment) lead to a dead end, it gives further insight into why the proof that flted_307_304 = 1 in #1 (comment) did not work. Recall that the proof is: "Firstly, we derive flted_307_304 >= 1 from int_arr_seg<flted_307_304> and the invariant inv n>=1 in the definition of pred int_arr_seg<n>. Secondly, we derive b_316 >= 0 from a>=0 & b>=0 in lemma "splitchar" self::arr_seg<a+b>. Thirdly, any flted_307_304>=2 violates the constraints flted_306_285 = 5, b_316 >= 0 and flted_306_285 = b_316 + 4(flted_307_304). So we conclude that flted_307_304 = 1."

Even though the proof is flawed, because flted_307_304 >= 1 is not derivable as #1 (comment) points out, we can still see the insight #1 (comment) gives: hipsleek cannot realize that "any flted_307_304>=2 violates the constraints flted_306_285 = 5, b_316 >= 0 and flted_306_285 = b_316 + 4(flted_307_304)", because hipsleek does not know flted_306_285 = b_316 + 4(flted_307_304). hipsleek only knows flted_306_285 = b_316 + a_315 for some uninstantiated a_315.

But even then, hipsleek should be able to enumerate all possible instantiations of a_315. Specifically, a_315 can only be instantiated to any number in 0,1,2,3,4,5. hipsleek should know this from the constraints flted_306_285 = 5, b_316 >= 0, a_315 >= 0 and flted_306_285 = b_316 + a_315. Indeed, z3 -smt2 file outputs unsat where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 0 b_316))
(assert (<= 0 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= flted_306_285 5))
;Negation of Consequence
(assert (not (and (<= 0 a_315) (<= a_315 5))))
(check-sat)

Recall that a_315=4*flted_307_304 is required to be proven for do_match@5 to succeed, as the predicate argumenta_315 must be instantiated to the other predicate argument 4*flted_307_304 for the match to occur. I suspect a_315=4*flted_307_304 not appearing in the input to Z3, indicates that hipsleek knows that proving 0 <= flted_307_304 <= 1 is equivalent to proving a_315=4*flted_307_304.

Indeed, running ./sleek -dre="compute_actions\|do_match" --pnum 32 --trace-log-num 5 testcases/ex5c.slk at 92c9796 with to a>=1 & b>=1 instead of a>=0 & b>=0 in lemma "splitchar" changes the consequent input to Z3 to @5!:0: 0: **smtsolver.ml#225:f(smt): y=x+4 & flted_306_285=5 & flted_307_304=1. So here, hipsleek knows that proving flted_307_304 = 1 is equivalent to proving a_315=4*flted_307_304. More precisely, omega knows that proving flted_307_304 = 1 is equivalent to proving a_315=4*flted_307_304, since flted_307_304 = 1 is output (as part of the consequent) from omega.

Here, hipsleek should be able to enumerate all possible instantiations of a_315. Specifically, a_315 can only be instantiated to any number in 1,2,3,4. hipsleek should know this from the constraints flted_306_285 = 5, b_316 >= 1, a_315 >= 1 and flted_306_285 = b_316 + a_315. Indeed, z3 -smt2 file outputs unsat where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 1 b_316))
(assert (<= 1 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= flted_306_285 5))
;Negation of Consequence
(assert (not (and (<= 1 a_315) (<= a_315 4))))
(check-sat)

Then, hipsleek should look at the structure of the original proof goal a_315=4*flted_307_304 (as opposed to the equivalent proof goal flted_307_304=1), to figure out that a_315 must be a multiple of 4. This is expressed in SMT-LIB as:

(declare-fun tmp () Int)
(assert (= a_315 (* 4 tmp)))

where we use tmp instead of flted_307_304 because we do not want to beg the question.

Then, the only possible instantiation for a_315 for the original proof to succeed is 4. Indeed, z3 -smt2 file outputs unsat where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun tmp () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 1 b_316))
(assert (<= 1 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= flted_306_285 5))
(assert (= a_315 (* 4 tmp)))
;Negation of Consequence
(assert (not (= a_315 4)))
(check-sat)

which is equivalent to

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
(declare-fun tmp () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 1 b_316))
(assert (<= 1 a_315))
(assert (= 1 flted_307_304))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= flted_306_285 5))
(assert (= a_315 (* 4 tmp)))
;Negation of Consequence
(assert (not (= a_315 (* 4 flted_307_304))))
(check-sat)

However, the equivalent proof that flted_307_304=1 cannot be shown from here. Along similar lines of thinking, z3 -smt2 file outputs sat where file is:

(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
(declare-fun tmp () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 1 b_316))
(assert (<= 1 a_315))
(assert (<= 1 flted_307_304))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= flted_306_285 5))
(assert (= a_315 (* 4 tmp)))
;Negation of Consequence
(assert (not (= a_315 (* 4 flted_307_304))))
(check-sat)

because Z3 thinks there can be flted_307_304 that when multiplied by 4 do not give a_315, and at the same time there is always tmp that when multiplied by 4 do give a_315. Indeed, for 1 <= a_315 <= 4, a tmp of 1 must constrain a_315 = 4, and then there are infinitely many flted_307_304 that when multiplied by 4 do not give a_315 i.e. 4, except for flted_307_304 of value 1.

Due to these failed attempts at handcrafting unsat SMT-LIB inputs, I suspect that it is impossible for Z3 to prove either a_315=4*flted_307_304 or flted_307_304=1. To justify, recall the Z3 input in testcases/ex5c.slk.trace-log-num_54.debug.geqno at #1 (comment):

(declare-fun b_306 () Int)
(declare-fun a_307 () Int)
(declare-fun q_308 () Int)
(declare-fun flted_306_277 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (= flted_306_277 (+ b_306 a_307)))
(assert (= (+ a_307 x) q_308))
(assert (= flted_306_277 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (= flted_306_277 5) (= y (+ x 4)))))
(check-sat)

There is no a_315=4*flted_307_304 or flted_307_304=1 in the consequence! So I suspect omega is extremely powerful in that it is able to eliminate those two proof goals for the *.geqno case, and omega is crucial for Z3 to output unsat and for the entailment to be valid.

from hipsleek.

Aside: the converse of entailment 32, checkentail x::int_arr_seg<1> * y::arr_seg<1> |- x::arr_seg<5> & y=x+4., is valid at 1b0a349 in both cases, one case with a>=0 & b>=0 in lemma "splitchar" and the other case without: because hipsleek now knows flted_306_285 = b_316 + 4(flted_307_304), because x::int_arr_seg<flted_307_304> is in the antecedent. However, the validity is also unsound in both cases:

[UNSOUNDNESS] WARNING : satisfiable state at 1 File "testcases/ex5c.slk",Line:307,Col:
14 became hfalse

Entail 32: Valid.

Residue:

 <1>hfalse&false&{FLOW,(20,21)=__norm#E}[]

Validate 32: OK

Interestingly, the converse of entailment 32, checkentail x::int_arr_seg<1> * y::arr_seg<1> |- x::arr_seg<5> & y=x+4., is invalid when a>=1 & b>=1 is in lemma "splitchar" at 92c9796.

from hipsleek.

At 92c9796, ./sleek --pcp --pnum 32 testcases/ex5c.slk outputs the data structure of the entailment:

INPUT 0: [][]
 ### ante =  x::arr_seg<flted_306_285>@M&flted_306_285=5 & y=4+x&
{FLOW,(20,21)=__norm#E}[]
 ### conseq =  EBase
   (exists flted_307_295,
   flted_307_296: x::int_arr_seg<flted_307_296>@M *
                  y::arr_seg<flted_307_295>@M&
   flted_307_296=1 & flted_307_295=1&{FLOW,(20,21)=__norm#E}[])

run_infer:
 x::arr_seg<flted_306_285>@M&flted_306_285=5 & y=4+x&
{FLOW,(20,21)=__norm#E}[] [] |-  EBase
   (exists flted_307_295,
   flted_307_296: x::int_arr_seg<flted_307_296>@M *
                  y::arr_seg<flted_307_295>@M&
   flted_307_296=1 & flted_307_295=1&{FLOW,(20,21)=__norm#E}[])

so we know flted_307_296 is existential, and we know by inspecting the proof tree to ./sleek -dre="compute_actions\|do_match\|Z3:check_formula" --pnum 32 --trace-log-num 55 testcases/ex5c.slk that flted_307_296 corresponds to flted_307_304 in here:

(====)
Z3:check_formula@56@55
Z3:check_formula inp1 :;Variables declarations
(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 1 b_316))
(assert (<= 1 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (and (= y (+ x 4)) (= flted_306_285 5)) (= flted_307_304 1))))
(check-sat)
Z3:check_formula inp2 :0.
Z3:check_formula@56 EXIT:sat

This motivates wrapping flted_307_304 in a existential. Indeed, z3 -smt2 file outputs unsat where file is:

;Variables declarations
(declare-fun b_316 () Int)
(declare-fun a_315 () Int)
(declare-fun q_314 () Int)
(declare-fun y () Int)
(declare-fun x () Int)
(declare-fun flted_306_285 () Int)
(declare-fun flted_307_304 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (<= 1 b_316))
(assert (<= 1 a_315))
(assert (= flted_306_285 (+ b_316 a_315)))
(assert (= (+ a_315 x) q_314))
(assert (= flted_306_285 5))
(assert (= y (+ 4 x)))
;Negation of Consequence
(assert (not (and (and (= y (+ x 4)) (= flted_306_285 5)) (exists ((flted_307_304 Int)) (= flted_307_304 1)))))
(check-sat)

So hipsleek forgets that flted_307_304 is an existential somewhere between converting the data structure of the entailment to a SMT-LIB input. Some commands run to debug where exactly hipsleek forgets are:

./sleek --pcp -dre="heap_entail\|Z3:check_formula" --pnum 32 testcases/ex5c.slk
./sleek --pcp -dre="heap_entail_empty_rhs\|Z3:check_formula" --pnum 32 testcases/ex5c.slk
./sleek --dd-calls-all --pcp -dre="heap_entail_empty_rhs\|Z3:check_formula" --pnum 32 testcases/ex5c.slk
./sleek --dd-calls-all --pcp -dre="heap_entail_empty_rhs\|Z3:check_formula\|imply\|elim_exists" --pnum 32 testcases/ex5c.slk
./sleek -dre="heap_entail_empty_rhs" --pnum 32 --trace-log-num 6 testcases/ex5c.slk
./sleek -dre="heap_entail_empty_rhs\|fold_fun_impt" --pnum 32 --trace-log-num 6 testcases/ex5c.slk
./sleek --dd-calls-all --pcp -dre="heap_entail_empty_rhs\|Z3:check_formula\|imply" --pnum 32 testcases/ex5c.slk
./sleek --dd-calls-all --pcp -dre="heap_entail_empty_rhs\|Z3:check_formula\|.*imply" --pnum 32 testcases/ex5c.slk
./sleek --pcp -dre="heap_entail\|Z3:check_formula\|do_match" --pnum 32 --trace-log-num 131 testcases/ex5c.slk

from hipsleek.