Skip to content

Conversation

NikolajBjorner
Copy link
Contributor

No description provided.

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor Author

@c-cube

@NikolajBjorner
Copy link
Contributor Author

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
Copy link
Contributor

c-cube commented Mar 23, 2020

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 :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants