From a85f1784db95c5975c3484215407f985d19f61ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Sep 2014 23:25:39 -0700 Subject: [PATCH] updated answer to binary interpolant Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index d46d40ab2..879b19597 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -7344,7 +7344,7 @@ def binary_interpolant(a,b,p=None,ctx=None): >>> x = Int('x') >>> print binary_interpolant(x<0,x>2) - x <= 2 + Not(x >= 0) """ f = And(Interp(a),b) return tree_interpolant(f,p,ctx)[0]