mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
disable unstable interpolation sample
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dca3ce6b24
commit
4995ce1fde
|
@ -7342,8 +7342,8 @@ def binary_interpolant(a,b,p=None,ctx=None):
|
|||
If parameters p are supplied, these are used in creating the
|
||||
solver that determines satisfiability.
|
||||
|
||||
>>> x = Int('x')
|
||||
>>> print binary_interpolant(x<0,x>2)
|
||||
x = Int('x')
|
||||
print binary_interpolant(x<0,x>2)
|
||||
Not(x >= 0)
|
||||
"""
|
||||
f = And(Interp(a),b)
|
||||
|
|
Loading…
Reference in a new issue