Fatal failure at theory/bv/bv_subtheory_algebraic.cpp:460 (bv-quick-xplain)

[rainoftime]

Hi,
For the following formula:

(set-logic QF_ABV)
(set-option :bv-quick-xplain true)
(declare-fun _substvar_97_ () Bool)
(declare-fun _substvar_104_ () (Array (_ BitVec 10) (_ BitVec 10)))
(declare-fun _substvar_114_ () (Array (_ BitVec 10) (_ BitVec 10)))
(declare-const v11 Bool)
(declare-const arr1 (Array (_ BitVec 10) (_ BitVec 10)))
(assert (xor (distinct true (xor true true true false v11 true false (= (store arr1 #b1000010111 #b1000010111) (store _substvar_104_ (bvsmod (select arr1 #b1000010111) #b1000010111) #b1000010111) arr1 _substvar_114_) false true) _substvar_97_ v11 false) true true true true true true true))
(check-sat)

CVC4 throws out a fatal failure:

 Fatal failure within bool CVC4::theory::bv::AlgebraicSolver::quickCheck(std::vector<CVC4::NodeTemplate<true> >&) at /home/peisen/test/tofuzz/CVC4/src/theory/bv/bv_subtheory_algebraic.cpp:460
 Check failure
 
  d_ids.find(c) != d_ids.end()

OS: Ubuntu 16.04
Commit: b9a903cc9a1

[ajreynol]

This code no longer exists.