Hi, For this formula: ``` (declare-fun a () (_ BitVec 9000)) (declare-fun b () (_ BitVec 9000)) (assert (bvslt a b)) (check-sat-using smt) ``` Z3 throws out a segmentation fault. OS: Ubuntu 18.04 Commit: dddd740