From 00ce124db3945b99e6d483891fa815bbcfa57f3a Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 2 Dec 2015 14:41:46 +0000
Subject: [PATCH] Bugfix for Z3_is_numeral for finite-domain numerals.

Relates to #318
---
 src/api/api_numeral.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
index d9064f423..770054870 100644
--- a/src/api/api_numeral.cpp
+++ b/src/api/api_numeral.cpp
@@ -149,7 +149,8 @@ extern "C" {
             mk_c(c)->autil().is_numeral(e) ||
             mk_c(c)->bvutil().is_numeral(e) ||
             mk_c(c)->fpautil().is_numeral(e) ||
-            mk_c(c)->fpautil().is_rm_numeral(e);
+            mk_c(c)->fpautil().is_rm_numeral(e) ||
+            mk_c(c)->datalog_util().is_numeral_ext(e);
         Z3_CATCH_RETURN(Z3_FALSE);
     }