sygus-inference ag-miniscope-quant fatal failure at src/theory/quantifiers/quantifiers_rewriter.cpp:1787

[muchang]

Hi,
For this formula:

(set-option :ag-miniscope-quant true)
(set-option :sygus-inference true)
(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ((c Real)) (or (< c a) (< 0 b))))
(check-sat)

CVC4 throws out a fatal failure:

Fatal failure within static CVC4::Node CVC4::theory::quantifiers::QuantifiersRewriter::computeAggressiveMiniscoping(std::vector<CVC4::NodeTemplate<true> >&, CVC4::Node) at src/theory/quantifiers/quantifiers_rewriter.cpp:1787
Check failure
 !qvl2.empty() || !qvsh.empty()
Aborted

OS: Ubuntu 18.04
Commit: a0b35a8