Segfault when using fresh variables in initial configuration

[Baltoli]

With the current design of the configuration initialisation mechanism, fresh variables won't work in the initial configuration as they rely on a cell being initialised.

I think the best thing to do here is just emit an error in the frontend if we detect fresh vars in the initial configuration; it might be possible to reorder calls and guarantee that initGeneratedCounterCell is called first, but I strongly suspect not.

Reproducing example:

module REPRODUCER-SYNTAX
  imports INT-SYNTAX
endmodule

module REPRODUCER
  imports DOMAINS
  imports REPRODUCER-SYNTAX

  configuration
    <k> $PGM:Int </k>
    <heap> !_:Int </heap>
endmodule

[dwightguth]

I agree we can just forbid this somehow. Nothing stops someone from just putting raw values of whatever sort they want fresh values in and then modifying the semantics to churn through values in order to sync the counters.

[Robertorosmaninho]

Closed with #3557