inexactJoins / Z3 timeout / assume() / resistor-01

- option -timeout x sets a max of x ms for each query. usually useful for
  a query that will _not_ succeed.

- assume(e) syntax, where e is intended to be a boolean-valued expression.

- if annotated var x /*: T */, then track _only_ that &x stores a T
  when joining a branch, rather than computing exact join.

    consider that the then branch with a guard b is

      e1 :: Exists y:T. S1/E1

    and E1 has a location (&x: vx) and &x has boundary invariant Tx.
    so, need to check

      G, truthy(b), y:T |- vx :: Tx

    but because Sub.types does binding of existentials more easily, instead
    check that

      G, truthy(b) |- Exists y:T. {v=vx} < Tx

- resistor-01.js runs in <20s.