Failure due to usage of function 'select'
Original issue created by @p.andrianov on 2016-01-19 at 12:29:29, last modified on 2016-01-21 at 10:01:08
In the rev. 17778 there was activated array support by SMTInterpol. Now CPAchecker fails while analyzing code which contains a function, which name is equal to the internal uninterpreted function name, like 'select'.
Exception in thread "main" de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Function select is already defined.
It seems, that CPAchecker should deal with this case. Anyway, is it possible to choose other logic? Now the code with logic set up is immutable. Very simple example is attached.