Extensions to Lustre input

Instantiate properties from called nodes in the calling node, and make sure every property of a node is an output by adding observer outputs.
Integrate path compression for k-induction.
Interpolate input streams of condacts between clock ticks.
Do some more checking to extend subranges. Fixes #121
Bugfixes in counterexample extraction. Fixes #123. Fixes #127