#2302 (Nov 18, 2020, 3:34:16 PM)

1. small changes and move debugging info to default solution warnings (commit: 44d86c6) (details / githubweb)
2. lint (commit: 1368695) (details / githubweb)
3. fix (commit: f0a03d3) (details / githubweb)
4. lint (commit: 5a27665) (details / githubweb)
5. TODOs and determinism (commit: 2dfb4e6) (details / githubweb)

GitHub pull request #1528 of commit 2dfb4e6d8a50f2de17fd3081fdc234781055902d, no merge conflicts.