With z3-4.8.8 (not the usual z3-4.3.2, because it does not have a string theory), autogenerated z3 code had a sort error in 60392cb from ./hip --smtinp testcases/ex5c-char2int.c, where in ex5c-char2int.c, s has type char *, but in the autogenerated z3 code, s_primed has sort String where s_primed was interpreted as a string variable, but s_primed has sort Int where s_primed was interpreted as a pointer variable (all pointers have sort Int):

dprint(simpl): testcases/ex5c-char2int.c:20: ctx:  List of Failesc Context: [FEC(0, 0, 1  [])]
 Successful States:
 [
  Label: []
  State:
     a_64::int_star<Anon_14>@M&MayLoop[] & a_64'=a_64&{FLOW,(4,5)=__norm#E}[]
    es_gen_impl_vars(E): []
    es_heap(consumed): emp
    es_subst (from,to): []:[]
    es_cond_path: [0]

  Exc:None
  ]
WARNING: _0:0_0:0:Z3 error message: (error "line 1377 column 26: Sorts Int and String are incompatible")
>>> GENERATED SMT INPUT:

;Variables declarations
(declare-fun a_64_primed () Int)
(declare-fun s_primed () Int)
(declare-fun a_64 () Int)
;Relations declarations
;Axioms assertions
;Antecedent
(assert true)
(assert (= a_64_primed a_64))
(assert (= s_primed "eypt"))
(assert (> s_primed 0))
(assert (> a_64 0))
;Negation of Consequence
(assert (not false))
(check-sat)

This sort error seems unresolvable without completely changing the autogeneration of z3 code, e.g. by moving all string assertions into a new, disjoint set of autogenerated code. This effort does not seem worth the benefit of reasoning with z3's string theory, because I believe it is enough to reason about primitive indexing into string pointers in the C programming language (corresponding to z3's (str.at s offset)). Then with this as a base, all other operations on strings (e.g. concatenation) can be verified by reasoning about C functions.

Note that the current hipsleek can already reason about primitive indexing into character arrays in the C programming language: character arrays are treated as integer pointers, and each character is treated as an integer. To make hipsleek reason about primitive indexing into strings, then, it remains to convert all strings into character arrays. This will be addressed in a future PR.

So I'm closing this PR for when someone wants to extend hipsleek's string reasoning abilities with z3's more complex string operations.