stp/stp — pull request #75 by s-falke (2014-02-21 15:22:37+00:00)
Title: When simplifying ITE, distinguish between array terms and other terms.

SimplifyingNodeFactory does some simplifications for ITE but always calls NodeFactory::CreateTerm instead of using NodeFactory::CreateArrayTerm if the ITE is an ITE for arrays. This causes FatalErrors to be triggered at a later stage. This fix introduces a distinction between ITE for arrays and ITE for booleans/bitvectors and calls the appropriate term creation method.

I'll try to come up with a testcase for this. I noticed this problem when using STP via its API in LLBMC (http://llbmc.org).