From 5fe4d88d43aefaf819ef50fa681e88df8ba0567d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 May 2026 13:08:54 -0700 Subject: [PATCH] recognize ubv_to_int as part of BV logic --- src/ast/bv_decl_plugin.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 76dc8fe07..bb65581cc 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -783,6 +783,9 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT)); op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT)); op_names.push_back(builtin_name("bit2bool", OP_BIT2BOOL)); + op_names.push_back(builtin_name("ubv_to_int", OP_UBV2INT)); + op_names.push_back(builtin_name("sbv_to_int", OP_SBV2INT)); + op_names.push_back(builtin_name("int_to_bv", OP_INT2BV)); if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD" || logic == "HORN") { op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL)); @@ -804,11 +807,10 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT)); op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT)); op_names.push_back(builtin_name("int2bv",OP_INT2BV)); - op_names.push_back(builtin_name("int_to_bv",OP_INT2BV)); + op_names.push_back(builtin_name("bv2int",OP_UBV2INT)); op_names.push_back(builtin_name("bv2nat",OP_UBV2INT)); - op_names.push_back(builtin_name("ubv_to_int",OP_UBV2INT)); - op_names.push_back(builtin_name("sbv_to_int",OP_SBV2INT)); + op_names.push_back(builtin_name("mkbv",OP_MKBV)); } }