Currently, if an unsatisfiable core references multiple Forge files, the entire core will be projected onto the currently open file in VSCode. (This behavior also seems to exist in Magic Racket with typed Racket's error messages.)
Relatedly, Forge reports the original model back to Sterling along with instances. This is useful for LLM integration, but only includes the top-level file, not any files that it imports. Thus, if file A opens file B, file B is not communicated to Sterling.
Currently, if an unsatisfiable core references multiple Forge files, the entire core will be projected onto the currently open file in VSCode. (This behavior also seems to exist in Magic Racket with typed Racket's error messages.)
Relatedly, Forge reports the original model back to Sterling along with instances. This is useful for LLM integration, but only includes the top-level file, not any files that it imports. Thus, if file A opens file B, file B is not communicated to Sterling.