From 3cefa0a1f76a4ce1cfe53fe5782aa8d061691535 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 5 Dec 2012 16:53:54 -0800
Subject: [PATCH] making tests deterministic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/api/python/z3.py | 17 ++++++++++++-----
1 file changed, 12 insertions(+), 5 deletions(-)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index e690a9bff..6517de221 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -5787,8 +5787,15 @@ class Solver(Z3PPObject):
>>> s.assert_and_track(x < 0, p3)
>>> print s.check()
unsat
- >>> print s.unsat_core()
- [p3, p1]
+ >>> c = s.unsat_core()
+ >>> len(c)
+ 2
+ >>> Bool('p1') in c
+ True
+ >>> Bool('p2') in c
+ False
+ >>> p3 in c
+ True
"""
if isinstance(p, str):
p = Bool(p, self.ctx)
@@ -6985,9 +6992,9 @@ def solve(*args, **keywords):
configure it using the options in `keywords`, adds the constraints
in `args`, and invokes check.
- >>> a, b = Ints('a b')
- >>> solve(a + b == 3, Or(a == 0, a == 1), a != 0)
- [b = 2, a = 1]
+ >>> a = Int('a')
+ >>> solve(a > 0, a < 2)
+ [a = 1]
"""
s = Solver()
s.set(**keywords)