Support for unsat core generation

[SimpleXiaohu]

For example below, ostrich can not generate right unsat core:

(set-option :produce-unsat-cores true)
(declare-const x String)
(declare-const i Int)
(assert (= x "hh"))
(assert (= i (str.len x)))
(assert (= i 1))

(check-sat)
(get-unsat-core)