On 11/14/2011 09:35 PM, Florian Haftmann wrote: >> @Florian: Is it imaginable to add such unsound setup >> in a way that it does not infect the evaluation oracle by default? > Indeed. More on that another time (when I find some time). > > Florian @Johannes: If you aim at adding another code target for this theory, I can assist with the setup. Lukas