Fatal failure at theory/quantifiers/sygus/ce_guided_single_inv.cpp:390 (ag-miniscope-quant, sygus-inference)

[rainoftime]

Related and fixed https://github.com/CVC4/CVC4/issues/4143

---

Hi, For the following formula:

(set-logic LIA)
(set-option :ag-miniscope-quant true)
(set-option :sygus-inference true)
(declare-fun _substvar_27_ () Bool)
(declare-fun _substvar_36_ () Bool)
(declare-const v2 Bool)
(assert (forall ((q2 Bool) (q3 Int) (q4 Int)) (xor q2 _substvar_36_ q2 q2 q2 true)))
(assert (or _substvar_27_ v2))
(check-sat)

CVC4 throws out a fatal failure:

 Fatal failure within bool CVC4::theory::quantifiers::CegSingleInv::solve() at /home/peisen/test/tofuzz/CVC4/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp:390
 Check failure

  qs.size() <= 1

OS: Ubuntu 16.04 Commit: b9a903cc9a1

[ajreynol]

Fixed on master.