The results of the above process are two systems of constraints;
real arithmetic constraints over
ownership variables and constrained Horn clauses (CHC) over the refinement relations.
Under certain assumptions about the simple types in a program, the size of the ownership
and subtyping constraints will be polynomial to the size of the program.
These systems are not independent; the relation constraints may mention the value
of ownership variables due to the well-formedness constraints described above.
The ownership constraints are first solved with Z3 [1]}. These constraints
are non-linear but Z3 appears
particularly well-engineered to quickly find solutions for the instances generated
by ConSORT.
We constrain Z3 to maximize the number of non-zero ownership
variables to ensure as few refinements as possible are constrained to be \( \top \)  by ownership well-formedness.
