Assertion error at solvers/quant/quant_solver.c:522

[rainoftime]

Hi, for the following formula, yices 426cdc6037

(set-logic UF)
(declare-fun uf4_2 (Bool Bool Bool Bool) Bool)
(declare-fun uf7_2 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(assert (uf7_2 true (not (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) q2)) true true true true true))
(assert (uf4_2 true true true true))
(check-sat)

$./yices_smt2 xx.smt2
yices_smt2: solvers/quant/quant_solver.c:522: term_substitution: Assertion `is_pos_term(x)' failed.

[dddejan]

CC @aman-goel