Package: z3 Version: 4.4.1-0.2 Hello, executing z3 on arm64 on the attached file produces a Segmentation fault, while it works fine on amd64. I didn't check any other architectures.
z3 -smt2 gauss-Gauss-WP_parameter_gauss.smt2 Segmentation fault -Ralf.
;;; generated by SMT-LIB2 driver ;;; SMT-LIB2 driver: bit-vectors, common part ;;; SMT-LIB2: integer arithmetic (declare-sort uni 0) (declare-sort ty 0) (declare-fun sort (ty uni) Bool) (declare-fun witness (ty) uni) ;; witness_sort (assert (forall ((a ty)) (sort a (witness a)))) (declare-fun int () ty) (declare-fun real () ty) (declare-fun bool () ty) (declare-fun match_bool (ty Bool uni uni) uni) ;; match_bool_sort (assert (forall ((a ty)) (forall ((x Bool) (x1 uni) (x2 uni)) (sort a (match_bool a x x1 x2))))) ;; match_bool_True (assert (forall ((a ty)) (forall ((z uni) (z1 uni)) (=> (sort a z) (= (match_bool a true z z1) z))))) ;; match_bool_False (assert (forall ((a ty)) (forall ((z uni) (z1 uni)) (=> (sort a z1) (= (match_bool a false z z1) z1))))) (declare-fun index_bool (Bool) Int) ;; index_bool_True (assert (= (index_bool true) 0)) ;; index_bool_False (assert (= (index_bool false) 1)) ;; bool_inversion (assert (forall ((u Bool)) (or (= u true) (= u false)))) (declare-sort tuple0 0) (declare-fun tuple01 () ty) (declare-fun Tuple0 () tuple0) ;; tuple0_inversion (assert (forall ((u tuple0)) (= u Tuple0))) ;; CompatOrderMult (assert (forall ((x Int) (y Int) (z Int)) (=> (<= x y) (=> (<= 0 z) (<= (* x z) (* y z)))))) (declare-fun ref (ty) ty) (declare-fun mk_ref (ty uni) uni) ;; mk ref_sort (assert (forall ((a ty)) (forall ((x uni)) (sort (ref a) (mk_ref a x))))) (declare-fun contents (ty uni) uni) ;; contents_sort (assert (forall ((a ty)) (forall ((x uni)) (sort a (contents a x))))) ;; contents_def (assert (forall ((a ty)) (forall ((u uni)) (=> (sort a u) (= (contents a (mk_ref a u)) u))))) ;; ref_inversion (assert (forall ((a ty)) (forall ((u uni)) (=> (sort (ref a) u) (= u (mk_ref a (contents a u))))))) (assert ;; WP_parameter_gauss ;; File "debian/tests/why/gauss.mlw", line 6, characters 8-13 (not (forall ((y Int)) (=> (< 0 y) (and (and (<= 0 y) (= (* 2 0) (* 0 (+ 0 1)))) (forall ((z Int) (x Int)) (=> (and (<= z y) (= (* 2 x) (* z (+ z 1)))) (ite (< z y) (forall ((z1 Int)) (=> (= z1 (+ z 1)) (forall ((x1 Int)) (=> (= x1 (+ x z1)) (and (and (<= z1 y) (= (* 2 x1) (* z1 (+ z1 1)))) (and (<= 0 (- y z)) (< (- y z1) (- y z)))))))) (= (* 2 x) (* y (+ y 1))))))))))) (check-sat)
