Hi,
For this formula:
(set-option :trace true)
(set-option :smt.arith.propagate_eqs false)
(set-option :smt.arith.random_initial_value true)
(set-option :smt.arith.eager_eq_axioms false)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< (* c (div b (+ a 2))) a))
(check-sat)
Z3 throws out a segmentation fault:
[505] % z3 small.smt2
Segmentation fault
[506] %
[506] % cat small.smt2
(set-option :trace true)
(set-option :smt.arith.propagate_eqs false)
(set-option :smt.arith.random_initial_value true)
(set-option :smt.arith.eager_eq_axioms false)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (< (* c (div b (+ a 2))) a))
(check-sat)
OS: Ubuntu 18.04
Commit: 9be7bda
Hi,
For this formula:
Z3 throws out a segmentation fault:
OS: Ubuntu 18.04
Commit: 9be7bda