Z3py从字符串创建Z3py表达式，或者：在eval中“not”会发生什么？

Question

我试图用Z3py来解决if或while语句中的约束。由于Z3py需要像True、False或Z3py Boolean expression这样的表达式，所以我必须解决如何将仅为字符串的约束转换为正确的形式。
我找到了这个主题，z3python: converting string to expression，它说应该使用“eval”。
现在，简而言之，我要做的是：

a = Real("a")
constr = "a < 1000"
ds = eval(constr)
print(ds)
solve(ds)

这很好地打印出：

real_a < 1000

[real_a = 0]

现在我还想解决这个约束的否定，即：

^{pr2}$

其结果是：

False

no solution

我真的不明白为什么会有这样的结果。我预期“not”中的整个表达式是颠倒的，因此解决方案将类似于“a=1000”。但显然情况并非如此。
现在我的问题是：这个结果到底发生了什么？而且，更重要的是：我该如何解决这个问题？有解决办法吗？
我知道我可以只更改every<；in>；=，ever>；in<；=，ever>；in or，或者反过来，删除every not等等。但这看起来有很多工作要做，我首先要确保没有其他方法。在