From f1d3a13b7f80ed84433c9890de3aa37484deff5e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Jul 2013 11:46:29 +0400 Subject: [PATCH] add missing case handlers for internal bit-vector operators that leak during simplification Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 6855f6209..293983c9a 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1073,6 +1073,12 @@ extern "C" { case OP_BSMUL_NO_OVFL: case OP_BUMUL_NO_OVFL: case OP_BSMUL_NO_UDFL: + case OP_BSDIV_I: + case OP_BUDIV_I: + case OP_BSREM_I: + case OP_BUREM_I: + case OP_BSMOD_I: + return Z3_OP_UNINTERPRETED; default: UNREACHABLE();