smt.arith.random_initial_value debug_ref_count trace proof; qfidl; Segmentation fault on QF_LRA formula

[muchang]

Hi,
For this formula:

(set-option :smt.arith.random_initial_value true)
(set-option :debug_ref_count true)
(set-option :trace true)
(set-option :proof true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(assert (= g a 0 i h))
(assert (distinct b (+ j f)))
(assert (= c (div l k e) d))
(check-sat-using qfidl)

Z3 gives a segmentation fault:

[711] % z3 small.smt2
Segmentation fault
[712] % 
[712] % cat small.smt2
(set-option :smt.arith.random_initial_value true)
(set-option :debug_ref_count true)
(set-option :trace true)
(set-option :proof true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(assert (= g a 0 i h))
(assert (distinct b (+ j f)))
(assert (= c (div l k e) d))
(check-sat-using qfidl)
[713] %

OS: Ubuntu 18.04
Commit: 9be7bda

[NikolajBjorner]

dup of #3594