From 5510e0ddef964a98eaba9f40e4b4a2e2a4899eb6 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 2 Dec 2015 17:03:37 +0000
Subject: [PATCH] Added finite-domain constant to Z3_decl_kind

---
 src/api/api_ast.cpp | 1 +
 src/api/z3_api.h    | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 5a35eecc8..de15c0c15 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -1098,6 +1098,7 @@ extern "C" {
             case datalog::OP_RA_COMPLEMENT: return Z3_OP_RA_COMPLEMENT;
             case datalog::OP_RA_SELECT: return Z3_OP_RA_SELECT;
             case datalog::OP_RA_CLONE:  return Z3_OP_RA_CLONE;
+            case datalog::OP_DL_CONSTANT: return Z3_OP_FD_CONSTANT;
             case datalog::OP_DL_LT: return Z3_OP_FD_LT;
             default:
                 UNREACHABLE();
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index d68fd9a1c..69fa0e9f0 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1155,6 +1155,7 @@ typedef enum {
     Z3_OP_RA_COMPLEMENT,
     Z3_OP_RA_SELECT,
     Z3_OP_RA_CLONE,
+    Z3_OP_FD_CONSTANT,
     Z3_OP_FD_LT,
 
     // Auxiliary