Regression between z3-4.8.8 and newer versions #5181
Description
We have been using z3 in CutEr, a concolic testing tool for Erlang, for some years now.
Yesterday, I've tried upgrading our z3 version from 4.8.8 to the latest release (4.8.10), and some of our unit tests fail. We were able to distill this to the following simple test:
; 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)which times out (loops) in the latest release (and also in 4.8.9), but was working correctly in all versions up to 4.8.8.
kostis:~$ ~/z3-4.8.3/build/z3 -smt2 -T:2 f.smt
sat
kostis:~$ ~/z3-4.8.7/build/z3 -smt2 -T:2 f.smt
sat
kostis:~$ ~/z3-4.8.8/build/z3 -smt2 -T:2 f.smt
sat
kostis:~$ ~/z3-4.8.10/build/z3 -smt2 -T:2 f.smt
timeout
kostis:~$ ~/z3-4.8.10/build/z3 -smt2 f.smt
LOOPSIs this a regression or something wrong in our test? (E.g., we are missing some option?)