From 60783e5696e4a741e7ff4aaeb4eb979d3c4bd77c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Jan 2017 13:26:58 -0800 Subject: [PATCH] fix regression for z3num Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c54cd6091..77b74336e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2394,7 +2394,7 @@ def is_int_value(a): >>> is_int_value(RealVal(1)) False """ - return isinstance(a, IntNumRef) + return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast()) def is_rational_value(a): """Return `True` if `a` is rational value of sort Real. @@ -2662,6 +2662,12 @@ class RatNumRef(ArithRef): return self.denominator().as_long() def is_int(self): + return False + + def is_real(self): + return True + + def is_int_value(self): return self.denominator().is_int() and self.denominator_as_long() == 1 def as_long(self):