Fatal failure on String formula at prop/cnf_stream.cpp:282

[rainoftime]

Related #4340
That test case is closed because it uses proof, which is not supported.

---

Hi,
For the following formula:

(declare-const i7 Int)
(declare-const Str8 String)
(declare-const Str17 String)
(assert (distinct (str.++ "" "rvhhcn" "" Str8 (int.to.str 56)) (str.++ "" (int.to.str i7) "" Str17) Str17))
(check-sat)

CVC4 throws out a fatal failure:

Fatal failure within CVC4::prop::SatLiteral CVC4::prop::CnfStream::getLiteral(CVC4::TNode) at /home/peisen/test/tofuzz/CVC4/src/prop/cnf_stream.cpp:282
Check failure

 d_nodeToLiteralMap.contains(node)
Literal not in the CNF Cache: (= (int.to.str i7) (str.++ dc_spt_7 dc_spt_rem_8))

Aborted (core dumped)

OS: Ubuntu 16.04
Commit: 2a38d48