Zenna Tavares

Write now all my functions take a context as a kwarg. This is cumbersome, and prone to the error of combining things which do not have the same context. Also...

``` julia #2 methods for generic function "model_eval": model_eval(ctx::Z3.Context, m::Z3.Model, t::Union{Z3.AppAst{T},Z3.Ast,Z3.FuncDeclAst,Z3.NumeralAst{T

Many types are just wrappers around a Ptr{Void}. It seems like these types can be initialised with anything, which led to some annoying bugs. I should prevent this so that...

``` julia A = Var(Integer) B = Var(Integer) add!(A * B == 12) check() model(Int, A) model(Int, B) #segfault here ```

The following causes memeory usage to increase rapidly, effectively forcing a hard restart ``` julia A = Var(Integer) add!(A > A) ```

ParametricInversion.jl currently relies on IRTools, Mjolnir, and the generated function trick to implement the inverse pass. This suffers from all of the well-known limitations of that approach: 1. It's unstable...

[PythonProgrammingPuzzles](https://github.com/microsoft/PythonProgrammingPuzzles/tree/main/puzzles) is a set of example programs expressed in Python. You're given a predicate, typically called `sat`, e.g. ```python def sat(s: str): """Find a string with 1000 'o's but no...