CHASE 0.3.0

• context=: formulas that every behavior satisfies (the axiom of an
  encoding of finite traces, a physical law), for the checks built on
  implication and satisfiability: implies, is_satisfiable,
  is_compatible, is_consistent, verify, refines,
  remove_redundant, accepts, implements, and unsat_core, also in
  the MCP server. The behaviors that violate the context are left out; as
  an assumption, the context would not help, since a behavior that
  violates an assumption satisfies the contract. See "Context" in
  docs/usage.md.
• load_spec and parse_spec warn when an integer is compared with a
  constant outside its range (e.g. credits >= 90 with credits declared
  without a range, so 0 to 16): the comparison has the same value at every
  step.
• The operations no longer leak memory. Before, every operation in Python
  (and every contract read from a file) kept the objects of the core
  library for good, 2 to 16 KB per operation. Now a contract owns its
  declarations and formulas, and a formula its operands, and chase_cps
  frees the objects of the core library once it has read the result
  (pychase.utilities.destroy). logics_tool: a proposition defined by a
  relation (proposition p is x > 3;) gets its own copy of the relation
  at each use, and a contract its own copy of the declarations of the
  system it uses.
• Core library: refinement put the formulas of the two contracts in the
  result instead of copies of them; saturating a contract with assumptions
  and no guarantees crashed (logics_tool saturate); the simplification
  turned a LargeOr of two formulas into an and.
• DSL_tool: computing the precision of the timings read one value past the
  end of an array (found by AddressSanitizer); the result was not used, and
  the specifications it writes are the same.
• CI: a job builds CHASE with AddressSanitizer and runs the Python tests
  and the console scripts of the demos.