From 2cd4669e2121009674025fe0d1a84aeb4070a820 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Jan 2015 01:47:57 -0800 Subject: [PATCH] add DT translation Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 04265af15..0ab027f69 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1076,7 +1076,6 @@ extern "C" { case OP_BSREM_I: case OP_BUREM_I: case OP_BSMOD_I: - return Z3_OP_UNINTERPRETED; default: UNREACHABLE(); @@ -1085,9 +1084,10 @@ extern "C" { } if (mk_c(c)->get_dt_fid() == _d->get_family_id()) { switch(_d->get_decl_kind()) { - case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR; - case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER; - case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR; + case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR; + case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER; + case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR; + case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD; default: UNREACHABLE(); return Z3_OP_UNINTERPRETED;