Seg fault with qfnra problem via OCaml API (fine via SMT-LIB, and had worked via OCaml API previously)

[grantpassmore]

The following qfnra problem is solved beautifully by z3 via SMT-LIB, but is crashing for us via the OCaml API. It's previously worked via the OCaml API with z3 4.8.5 (we're just now upgrading to 4.8.8):

(declare-fun x_34 () Real)
(declare-fun b_32 () Real)
(declare-fun a_31 () Real)
(assert (let ((a!1 (or (<= a_31 0.0)
               (<= (* (- 1.0) a_31 b_32 b_32)
                   (+ (* a_31 x_34 x_34) (* (- 2.0) a_31 b_32 x_34))))))
  (not a!1)))
(check-sat-using qfnra)

I attach a .log file obtained from our run via OCaml, which reproduces the seg fault when I run it via z3 -log. Let me know please if I can provide anything else. Thanks so much!

z3.log

BTW, this .log file was created with z3 at commit 8439057.

[NikolajBjorner]

Your ocaml mode sets proof to "true". It also sets unsat_core to "true", which is not supported from the front-end (but bypassed from binary mode).
Changing proof mode to "false" in the log avoids the assertion violation (crash). Changing unsat_core to false, but keeping proof=true still crashes so there are maybe some other things in play (factor, reorder, elim_and?).