Testing that a constant matches an interval

Question

Given the following simple example:

s = Solver()

Z = IntSort()
a = Const('a', Z)

s.add(a >= 0)
s.add(a < 10)

print(s.check(a > 5)) # sat

Up until the last line, a has an implied range of 0 <= a < 10 - for which a > 5 does not satisfy. However, .check() tells z3 that "this is true" - which is not what I'm after.

Is there a way to ask z3 to test if a > 5 given the existing set of constraints, and have z3 interpret this as "make sure this is true given everything else we know about a"?

---

EDIT: Okay I think I figured it out. Since z3 tries to find a model that satisfies all constraints, I should instead check for the inverse to see if it finds a solution - in which case, my check would not hold.

In this case, my "test" function would become:

def test(s, expr):
    return s.check(Not(expr)) == unsat

thus...

s = Solver()

Z = IntSort()
a = Const('a', Z)

s.add(a >= 0)
s.add(a < 10)

print(s.check(a > 5)) # sat

print(s.check(Not(a > 5)) == unsat) # false, test failed
s.add(a > 8)

print(s.check(Not(a > 5)) == unsat) # true, test passed

Is that correct?