Upgrade to latest z3 (4.8.14)

[kostis]

No description provided.

[aggelgian]

; z3 -smt2 -T:2 -in
(set-option :produce-models true)
; Erlang types.
(declare-datatypes () ((Term (int (iv Int)) (real (rv Real)) (list (lv TList)) (tuple (tv TList)) (atom (av IList)) (str (sv SList)) (fun (fv Int))) (TList (tn) (tc (th Term) (tt TList))) (IList (in) (ic (ih Int) (it IList))) (SList (sn) (sc (sh Bool) (st SList))) (FList (fn) (fc (fx TList) (fy Term) (ft FList)))))
(declare-const x Term)
(define-fun-rec fun-rec-0 ((l TList)) Bool (or (is-tn l) (and (is-tc l) true (fun-rec-0 (tt l)))))
; Type signature for argument.
(assert (and (is-list x) (fun-rec-0 (lv x))))
; Two terms are not equal.
(assert (not (= (list tn) x)))
; Term is a non-empty list.
(assert (and (is-list x) (is-tc (lv x))))
(declare-const y Term)
; T0 = hd(T1).
(assert (and (is-list x) (is-tc (lv x)) (= y (th (lv x)))))
(declare-const z Term)
; T0 = tl(T1).
(assert (and (is-list x) (is-tc (lv x)) (= z (list (tt (lv x))))))
; Two terms are equal.
(assert (= (list tn) z))
(check-sat)

➜  cuter git:(z3-4.8.10) ✗ z3 --version && z3 -smt2 -T:2 f.smt
Z3 version 4.8.10 - 64 bit
timeout

➜  cuter git:(z3-4.8.10) ✗ z3 --version && z3 -smt2 -T:2 f.smt
Z3 version 4.8.8 - 64 bit
sat

➜  cuter git:(z3-4.8.10) ✗ z3 --version && z3 -smt2 -T:2 f.smt             
Z3 version 4.8.9 - 64 bit
timeout