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