Non-deterministic assertion violation at btorslvquant.c:1049

[rainoftime]

Hi, for the following formula,

(set-logic BV)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(assert (forall ((q0 Bool) (q1 Bool) (q2 Bool)) (not (and q1 q0 v0 q1 q2))))
(assert (or v1 v4))
(check-sat)

boolector (commit 59c9ade) throws an assertion violation

boolector: /home/boolector/src/btorslvquant.c:1049: refine_exists_solver: Assertion `res != e_solver->true_exp' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted

option

boolector --engine=quant --quant-synth=elmr file.smt2

The default option boolector file.smt2 may also trigger the issue.

seq 10 | xargs -Iz /home/boolector/build/bin/boolector  xx.smt2
sat
sat
sat
sat
boolector: /boolector/src/btorslvquant.c:1049: refine_exists_solver: Assertion `res != e_solver->true_exp' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
xargs: /home/boolector/build/bin/boolector: terminated by signal 6