todo

- Overall
  - Separate Language.Boogie library from Boogaloo
  
- Library  
  - AST and parser
    - Unsupported syntax
      - bit vectors    
      - reals, /, **, int(), real(), decimal/float litearls
      - call * := Q(x, y), call forall to a procedure with out-parameters
      - empty map domains x: []int    
      - code expression
    - Optimization: e.g. better data structures instead of lists and strings  
    - Do not throw away attributes and triggers

    - Type checker
      - Annotate AST with expr types
      - Use semantic representation of types not just for comparison?
      - Data type for type errors (will be easier to evaluate test results)
      - Use lenses for Context?      
  
- Boogaloo
  - Collect unused maps
  - Make fair strategy work again
  - Alternative way of fixing Bubble bug: concretize all map indices?
  - Extract map constraints from nonsimple arguments
  - Take into account extends ordering
  - Fix loop_max parameter (currently jumps are summed up from all recursive calls, needed to make recursion work with DFS)
  - Fix rec_max parameter (currently does not check unguarded constraints)
  
  - User interface
    - When violated spec has logical vars, output their values  
    - Turn source positions into spans; use the end of the span to report postcondition violations