From 282834f90f84a951990503ba2b4d1958bebe1947 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 17 Feb 2026 21:17:42 +0000 Subject: [PATCH] delete dead code --- src/ast/bv_decl_plugin.h | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 6bfc50898..225fda0d6 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -118,26 +118,6 @@ enum bv_op_kind { LAST_BV_OP }; -// Assume k is a "div" operator. It returns the div0 uninterpreted function that -// models the value of "div" it is underspecified (i.e., when the denominator is zero). -inline bv_op_kind get_div0_op(bv_op_kind k) { - switch (k) { - case OP_BSDIV: return OP_BSDIV0; - case OP_BUDIV: return OP_BUDIV0; - case OP_BSREM: return OP_BSREM0; - case OP_BUREM: return OP_BUREM0; - case OP_BSMOD: return OP_BSMOD0; - default: UNREACHABLE(); return LAST_BV_OP; - } -} - -// Assume decl is the declaration of a "div" operator. It returns the div0 declaration that -// models the value of "div" it is underspecified (i.e., when the denominator is zero). -inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) { - return m.mk_func_decl(decl->get_family_id(), get_div0_op(static_cast(decl->get_decl_kind())), - 0, nullptr, 1, decl->get_domain()); -} - class bv_decl_plugin : public decl_plugin { friend class bv_util; protected: