Fix of #1 is incomplete about hipsleek HOT 2 OPEN

An attempted fix of this issue at 53e7656 causes a timeout and hence an invalid entailment, as in issues-1.slk.add_push_pop.not_on_reset (in contrast with issues-1.slk.add_push_pop.always) at commit df7a1f2.

from hipsleek.

The fix of issue #2 at 5ae020a makes valid the entailment 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>. as in #1 (comment).

One of the original goals of the analysis in issue #1 is to verify that lemma "int2char" is safe. However, both folding lemmas lemma_safe "int2char" self::int_arr_seg<n> & m=2*n <- self::arr_seg<m>. as in #1 (comment) and lemma_safe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n. as in 9d5576d, when checked for safety, still give Entailing lemma int2char: Fail. (cex)(may) cause: OrL[residue is forbidden.(1), valid]. Specifically, the inductive case cannot be verified to be safe.

from hipsleek.