sygus-inference quant-cf fs-interleave cbqi-all arith-rewrite-equalities ag-miniscope-quant Fatal failure at src/theory/quantifiers/term_database.cpp:878

[muchang]

Hi,
For this formula:

(set-option :sygus-inference true)
(set-option :quant-cf true)
(set-option :fs-interleave true)
(set-option :cbqi-all true)
(set-option :arith-rewrite-equalities true)
(set-option :ag-miniscope-quant true)
(declare-fun a (Bool Bool Bool Bool Real Real Real Real Real Real Real Real
        Real Real Real Real Real Real Real Real Real Real Real) Bool)
(assert
 (forall ((b Bool)
     (b1 Bool)
     (b2 Bool)
     (b3 Bool)
     (c Real)
     (abaa Real)
     (d Real)
     (acaa Real)
     (eaa Real)
     (adaa Real)
     (faa Real)
     (aeaa Real)
     (afaa Real)
     (g Real)
     (e Real)
     (h Real)
     (i Real)
     (ahaa Real)
     (aiaa Real)
     (f Real)
     (k Real)
     (l Real)
     (j Real)
     (aiaaaj Real)
     (laj Real)
     (aj Real)
     (faj Real)
     (jaj Real)
     (kaj Real)
     (ahaaaj Real)
     (haaaj Real)
     (caj Real)
     (abaaaj Real)
     (daj Real)
     (acaaaj Real)
     (eaaaj Real)
     (adaaaj Real)
     (faaaj Real)
     (aeaaaj Real)
     (afaaaj Real)
     (gaj Real)
     (eaj Real)
     (haj Real)
     (iaj Real)
     (baj Bool)
     (m Real))
 (=> (and (a b b1 b2 b3 c abaa d acaa eaa adaa faa aeaa afaa g e h i ahaa aiaa f k l j)
    (or (and (and (not (= m 0))(not b))(= faa faaaj) b2)
    (and (= i aiaa h ahaa) (= e g afaa afaaaj aeaa adaa eaa acaa d c abaa f k l j))))
  (a baj b1 b2 b3 aj abaaaj daj acaaaj eaaaj adaaaj faaaj aeaaaj afaaaj gaj eaj haj
  iaj haaaj aiaaaj faj kaj laj jaj))))
(check-sat)

CVC4 throws out a fatal failure:

Fatal failure within bool CVC4::theory::quantifiers::TermDb::isEntailed(CVC4::TNode, bool, CVC4::theory::EqualityQuery*) at src/theory/quantifiers/term_database.cpp:878
Check failure
 d_consistent_ee
Aborted

OS: Ubuntu 18.04
Commit: 92ed768

[ajreynol]

Now times out without assertion failure.