Currently if you run saw multiple times or from different checkouts, the output varies. Ideally the results would be fully repeatable. This is desirable for testing and also for differential analysis of bugs and so forth.
Some solver-based things may not be fully repeatable without significant intervention and that may not be worthwhile (for example, exact counterexamples for verification failures) but there are at least two things that currently vary that could be nailed down quite easily:
[ ] Timestamps. Right now all outputs are timestamped; this is sometimes useful but should be suppressible.
[ ] Filenames. Currently saw runs realpath on filenames, which it probably shouldn't at all (see #2082). This introduces the current directory (which is often, especially when testing/developing, the path of the current saw-script checkout) into the output. At a minimum, in repeatable mode it ought to prune the current directory from the filenames it prints.
Currently if you run saw multiple times or from different checkouts, the output varies. Ideally the results would be fully repeatable. This is desirable for testing and also for differential analysis of bugs and so forth.
Some solver-based things may not be fully repeatable without significant intervention and that may not be worthwhile (for example, exact counterexamples for verification failures) but there are at least two things that currently vary that could be nailed down quite easily: