Enter a source monotone problem

This will be defunctionalized into a first-order monotone problem and be solved using Z3. See GitHub for the implementation.
Test cases: ack a-max-e a-max hrec max mc91-e mc91 mult-e mult neg repeat-e sum-e sum hold

submit

Target monotone problem

Z3 Output