[SAL-HELP] How to read new assertions using sal-sim?

[Gordon Fraser]

Hi,

Is it possible to model check LTL properties that are not included in
the SAL context originally parsed? I am interacting with sal-sim through
a pipe, and would like to check deliberate properties. When I've got
named assertions I can see how it's done, but I couldn't figure out how
to add new assertions with LTL expressions. I suppose this is easy but
my insufficient Scheme skills prevent me from finding the solution. Any
hints or pointers would be greatly appreciated.

Thanks,
Gordon