Use a composite z3 formula as output from kclause when running klocalizer.

[paulgazz]

Currently, kclause converts the constraints for each configuration option to the smtlib format separately, which is roughly half of the running time of kclause. Since klocalizer combines these constraints anyway, add an option to output the composite version and update klocalizer to use this, since it composites the formula anyway.

This requires some care when using with kismet and other tools which may expect the original output of kclause.