Fix of #1 is incomplete

[zhengqunkoo]

issues-1.slk.iget_answer.rec at commit c937a7f61 probably has the correct ouput by chance, because 2e37560cc has a bug that is not manifested: when (reset) is used, the input to Z3 is, given by new_f at line https://github.com/zhengqunkoo/hipsleek/blob/2e37560cc045923f1b3804cf4e2fc4a87865c58e/smtsolver.ml#L751, as in:

(push)
(reset)
;Variables declarations
(declare-fun n () Int)
(declare-fun f () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert (< 1 n))
(assert (= (+ (+ 1 f) 1) (+ n n)))
(assert (<= 2 f))
;Negation of Consequence
(assert (not (exists ((alpha_134 Int)) (= (* 2 alpha_134) f))))
(check-sat)(pop)

on which running z3 -smt2 gives:

unsat
(error "line 14 column 15: invalid pop command, argument is greater than the current stack depth")

which could have unintended consequences. The solution is to remove (push) and (pop) from new_f whenever (reset) is used. A similar problem likely manifests at new_f at line https://github.com/zhengqunkoo/hipsleek/blob/2e37560cc045923f1b3804cf4e2fc4a87865c58e/smtsolver.ml#L1313.

[zhengqunkoo]

An attempted fix of this issue at 53e765607 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 df7a1f2a8.

[zhengqunkoo]

The fix of issue #2 at 5ae020ae4 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 https://github.com/zhengqunkoo/hipsleek/issues/1#issuecomment-664789560.

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 https://github.com/zhengqunkoo/hipsleek/issues/1#issuecomment-664789560 and lemma_safe "int2char" self::int_arr_seg<n> <- self::arr_seg<m> & m=2*n. as in 9d5576d59, 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.