Rs

[NikolajBjorner]

No description provided.

[NikolajBjorner]

@c-cube

[NikolajBjorner]

from z3 import *
x = Int('x')
p = Lambda([x], x >= 0)
Nat = RefineSort(p)
n, m = Consts('n m', Nat)
s = Solver()
s.add(Relax(n) + Relax(m) < 0)
print(s.check())
#print(s.reason_unknown())
#print(s.model())

[c-cube]

That looks pretty good. I'll give it a try when I'm less swamped (btw I hope y'all are ok in the WA area…).

I do need this in the OCaml API though :)